[Haskell-cafe] Type family weirdness

[David Feuer]

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 <eir at cis.upenn.edu> wrote:
> Looks like a bug. I think the `coercionXX = Coercion` should work.
>
> Richard
>
> On Dec 5, 2015, at 9:58 PM, David Feuer <david.feuer at gmail.com> 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 at haskell.org
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>>
>