#8984: Improve output of failed GeneralizedNewtypeDeriving coercion due to type roles --------------------------------------------+------------------------------ Reporter: haasn | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type checker) | Version: 7.8.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Test Case: | Difficulty: Unknown Blocking: | Blocked By: | Related Tickets: --------------------------------------------+------------------------------ Comment (by simonpj): Here's a small test case {{{ {-# LANGUAGE ConstraintKinds, GeneralizedNewtypeDeriving #-} module T8984 where class C a where app :: a (a Int) newtype N cat a b = MkN (cat a b) deriving( C ) -- The newtype coercion is N cat ~R cat }}} We try to prove `Coercible (cat (cat Int) (N cat (N cat Int))`. We simplify this (by newtype unrwrapping) to `Coercible (cat (cat Int)) (cat (N cat Int))`; and now we are stuck. {{{ T8984.hs:7:46: Could not coerce from ‘cat a (cat a Int)’ to ‘cat a (N cat a Int)’ because ‘cat a (cat a Int)’ and ‘cat a (N cat a Int)’ are different types. arising from the coercion of the method ‘app’ from type ‘cat a (cat a Int)’ to type ‘N cat a (N cat a Int)’ }}} An alternative strategy would be to see that the newtype axiom is over- applied, and instead decompose the application thus: {{{ Coercible (cat (cat Int) (N cat (N cat Int)) ==> (decompose application into two parts) Coercible cat (N cat), cat Int ~ N Cat int }}} Now the first constraint is soluble, but the second would say something like "cannot deduce `cat Int ~ N Cat Int`. Joachim, Richard, thoughts? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8984#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler