Improve GADT type inference
It'd be nice if programs like the following didn't require type annotations:
data PromptR (r :: * -> *) (a :: *) where
NewRef :: a -> PromptR r (r a)
Fetch :: r a -> PromptR r a
Set :: r a -> a -> PromptR r ()
-- prIO :: PromptR IORef a -> IO a
prIO (NewRef a) = newIORef a
prIO (Fetch r) = readIORef r
prIO (Set r v) = writeIORef r v
I get the following cryptic error message:
prompt.lhs:193:7:
Couldn't match kind `?' against `* -> *'
When matching the kinds of `t :: ?' and `t1 :: * -> *'
Expected type: t1
Inferred type: t
In the pattern: NewRef a
It seems to me you shouldn't need a type annotation here:
prIO (NewRef a) = newIORef a
therefore:
prIO :: x -> y
x ~ PromptR r z
in this case only:
z ~ (r a), a :: a (from GADT argument)
newIORef :: b -> IO (IORef b)
a ~ b
y ~ IO (IORef a) | r ~ IORef, y ~ IO (r a)
prIO (Fetch r) = readIORef r
in this case only:
r :: r z (from GADT argument)
readIORef :: IORef b -> IO b
r ~ IORef
b ~ z
y ~ IO z
attempt to unify with above case, and we get
x ~ PromptR r z
y ~ IO z
r ~ IORef
prIO :: PromptR IORef z -> IO z
is the least specific possibility that matches both cases.
Interestingly, if I include only the second case, the type is inferred successfully; if I include the second and third cases, the type is inferred incorrectly as PromptR IORef () -> IO ()
P.S. I only tested this on GHC6.6.1; apologies if this already works in 6.8.
Trac metadata
Trac field | Value |
---|---|
Version | 6.6.1 |
Type | FeatureRequest |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler (Type checker) |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | ryani.spam@gmail.com |
Operating system | Unknown |
Architecture | Unknown |