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