Skip to content

Odd interaction between type families and coercions (regression)

{-# LANGUAGE TypeFamilies #-}

module Wonk where
import Data.Type.Coercion

type family X

coercionXX :: Coercion X X
coercionXX = Coercion

This works just fine in 7.8.3, but in 7.10.2 it gives the following peculiar error:

    Couldn't match representation of type ‘X’ with that of ‘X’
    NB: ‘X’ is a type function, and may not be injective
    In the expression: Coercion
    In an equation for ‘coercionXX’: coercionXX = Coercion

I don't even know what it means for a nullary type family to be injective. I tried the following workarounds:

coercionXX1 :: Coercion X X
coercionXX1 = c where
  c :: x ~ X => Coercion x x
  c = Coercion

coercionXX2 :: Coercion X X
coercionXX2 = c where c = Coercion

Interestingly, coercionXX1 seems to work under all circumstances, with or without the top-level type signature; coercionXX2 works if it's in a .hs file, but does not work if entered by hand at the ghci prompt (it produces a similar error).

Edited by David Feuer
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information