In case this helps any, coercionXX = c where c :: x ~ X => Coercion x x c = Coercion works too (with or without a top-level type signature), but coercionXX = c where c :: Coercion X X c = Coercion gives the same error as before. On Sat, Dec 5, 2015 at 11:51 PM, Richard Eisenberg wrote:

Looks like a bug. I think the `coercionXX = Coercion` should work.

Richard

On Dec 5, 2015, at 9:58 PM, David Feuer wrote:

...

If I have

{-# LANGUAGE PolyKinds, TypeFamilies #-} import Data.Type.Coercion

type family X :: k

and I want

coercionXX :: Coercion X X,

the obvious thing,

coercionXX = Coercion,

doesn't work:

Couldn't match representation of type ‘X’ with that of ‘X’ NB: ‘X’ is a type function, and may not be injective Relevant role signatures: type role X nominal Relevant bindings include coercionXX :: Coercion X X (bound at Fold.hs:167:1) In the expression: Coercion In an equation for ‘coercionXX’: coercionXX = Coercion

However, if I write

coercionXX = x where x = Coercion,

that does work! What gives? _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe