#1991: Improve GADT type inference
----------------------------------------+-----------------------------------
Reporter: guest | Owner:
Type: feature request | Status: new
Priority: normal | Milestone:
Component: Compiler (Type checker) | Version: 6.6.1
Severity: normal | Keywords:
Difficulty: Unknown | Testcase:
Architecture: Unknown | Os: Unknown
----------------------------------------+-----------------------------------
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.
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/1991>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler_______________________________________________
Glasgow-haskell-bugs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
