[Haskell-cafe] interesting type families problem

[Gábor Lehel]

I'm bad at expositions so I'll just lead with the code:

{-# LANGUAGE EmptyDataDecls, TypeFamilies #-}

data True  :: *
data False :: *

class TypeValue a where
    type ValueTypeOf a :: *
    value :: ValueTypeOf a

instance TypeValue True where
    type ValueTypeOf True = Bool
    value = True

instance TypeValue False where
    type ValueTypeOf False = Bool
    value = False

main = print (value :: ValueTypeOf True)

(In case this is initially confusing, there are entirely distinct
type-level and value-level True and False involved which merely share
a name. The idea is to take type-level 'values' and reflect them down
to the corresponding value-level, er, values.)

Which results in the following error message:

    Couldn't match expected type `Bool'
           against inferred type `ValueTypeOf a'
      NB: `ValueTypeOf' is a type function, and may not be injective
    In the first argument of `print', namely
        `(value :: ValueTypeOf True)'
    In the expression: print (value :: ValueTypeOf True)
    In the definition of `main':
        main = print (value :: ValueTypeOf True)


This is strange and vaguely amusing to me. I get that type functions
are not injective, but I can't figure out how it applies to this
situation. Obviously if I had written `print (value :: Bool)` it would
rightly complain that there could be any number of instances which map
to Bool, and how in the world should it know which one I meant. But it
seems like in this case the compiler knows everything it needs to
know. And it even manages to deduce, from the exact same expression
(`print` isn't giving it any extra information), that it's
simultaneously a Bool and not necessarily a Bool.

Is this "supposed" to work? If not, why not?


-- 
Work is punishment for failing to procrastinate effectively.