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 |