Skip to content
Snippets Groups Projects

Odd interaction between type families and coercions (regression)

    • Closed Issue created by David Feuer @treeowl 
    {-# 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
    To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information

    Child items 0

    • No child items are currently assigned. Use child items to break down this issue into smaller parts.

    Activity

    Please register or sign in to reply