Type variables allowed to unify in a partial type signature (PartialTypeSignatures)
During a discussion today, Richard discovered the following bug:
The function f
is accepted in GHC 8.2.1 (and HEAD too):
{-# LANGUAGE PartialTypeSignatures #-}
f :: a -> b -> _
f x y = [x, y]
with the warning:
Bug.hs:3:16: warning: [-Wpartial-type-signatures]
• Found type wildcard ‘_’ standing for ‘[a]’
Where: ‘a’ is a rigid type variable bound by
the inferred type of f :: a -> a -> [a] at Bug.hs:4:1-13
• In the type signature: f :: a -> b -> _
|
3 | f :: a -> b -> _
| ^
Ok, 1 module loaded.
This is a regression compared to 8.0.1, where the following error is produced (rightly):
Bug.hs:4:12: error:
• Couldn't match expected type ‘a’ with actual type ‘b’
‘b’ is a rigid type variable bound by
the inferred type of f :: a -> b -> [a]
at Bug.hs:3:6
‘a’ is a rigid type variable bound by
the inferred type of f :: a -> b -> [a]
at Bug.hs:3:6
• In the expression: y
In the expression: [x, y]
In an equation for ‘f’: f x y = [x, y]
• Relevant bindings include
y :: b (bound at Bug.hs:4:5)
x :: a (bound at Bug.hs:4:3)
f :: a -> b -> [a]
(bound at Bug.hs:4:1)
Failed, modules loaded: none.
Note that the inferred type of f
is still correct: f :: a -> a -> a
, but the type variables a
and b
are allowed to unify during inference, and they shouldn't be. If I understood correctly, this implies that when inferring the type of functions with partial type signatures, the type variables are (wrongly) treated as SigTv
s, instead of skolem constants.
Trac metadata
Trac field | Value |
---|---|
Version | 8.2.1 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler (Type checker) |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | goldfire, simonpj |
Operating system | |
Architecture |