Weak inference when using rank-2 types and type families.

Type inference does work as expected, when a rank-2 type has 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.

Trac metadata

Trac field	Value
Version	7.10.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture