Trivial partial type signature kills type inference in the presence of GADTs
Suppose we have
data G a where
G1 :: G Char
G2 :: G Bool
If I now write
foo x = case x of
G1 -> 'z'
G2 -> True
I rightly get an error around untouchable variables.
If I add the type signature
foo :: G a -> a
all is well again. So far, so good.
Now, I write
foo :: forall a. G a -> a
foo x = ((case x of
G1 -> 'z'
G2 -> True) :: _)
and I get those untouchable errors again. Untouchable-variable errors usually arise when there are multiple possible answers to the type inference problem. Yet, that isn't the case here: _
must stand for a
.
Solution: mumble mumble bidirectional type inference mumble mumble.
Part of the problem comes from Note [Partial expression signatures] in TcExpr, which states
here is a guiding principile
e :: ty
should behave like
let x :: ty
x = e
in x
Indeed, if we behave like that, the untouchable-variable errors are to be expected. But I also think that it would be a nice principle to say that :: _
is always a no-op.
This is not an idle nice-to-have: if we fix this, singletons
will continue to work with GHC. Right now, it doesn't: https://github.com/goldfirere/singletons/issues/357
Trac metadata
Trac field | Value |
---|---|
Version | 8.6.3 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |