[Haskell-cafe] Type family weirdness

[Richard Eisenberg]

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
>