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 |