Odd interaction between rank-2 types and type families
Type inference does not work as expected, when a rank-2 type has a type-family constraint. Consider the following program:
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE Rank2Types #-}
type family F a
f :: (forall s. (F s ~ Int) => s -> b) -> b
f _ = undefined
k :: s -> Char
k = undefined
example :: Bool
example = const True (f k)
It is rejected with the following error:
Couldn't match type ‘b0’ with ‘Char’
‘b0’ is untouchable
inside the constraints (F s ~ Int)
bound by a type expected by the context: (F s ~ Int) => s -> b0
at bug.hs:13:23-25
Expected type: s -> b0
Actual type: s -> Char
In the first argument of ‘f’, namely ‘k’
In the second argument of ‘const’, namely ‘(f k)’
This is unexpected because the result of f
should be the same as
the result of its parameter, and we know the exact type of the parameter, namely Char
.