RE: [GHC] #7766: equality constraints exposed by patterns mess up constraint inference
You probably need
do { (case .... of ...) :: IO ()
; return () }
It's not a bug, in other words. The "modular type inference with local constraints" paper is a good reference here.
Simon
| -----Original Message-----
| From: Gabor Greif [mailto:ggreif@gmail.com]
| Sent: 13 March 2013 15:05
| To: ghc-devs@haskell.org; Simon Peyton-Jones
| Cc: ghc-tickets@haskell.org
| Subject: Re: [GHC] #7766: equality constraints exposed by patterns mess
| up constraint inference
|
| Hi Simon,
|
| okay, I see how a type signature will help in that case, but it is
| unclear where to add one in this (even simpler) example:
|
|
| {-# LANGUAGE GADTs, DataKinds, KindSignatures #-}
|
| data Nat = S Nat | Z
|
| data Nat' (n :: Nat) where
| S' :: Nat' n -> Nat' (S n)
| Z' :: Nat' Z
|
| main :: IO ()
| main = do case S' Z' of
| (S' Z') -> putStrLn "yep" -- see error message below...
| -- _ -> putStrLn "yep" -- works!
| return ()
|
| {-
| [1 of 1] Compiling Main ( pr7766.hs, pr7766.o )
|
| pr7766.hs:11:23:
| Couldn't match type `a0' with `()'
| `a0' is untouchable
| inside the constraints (n ~ 'Z)
| bound by a pattern with constructor
| Z' :: Nat' 'Z,
| in a case alternative
| at pr7766.hs:11:16-17
| Expected type: IO a0
| Actual type: IO ()
| In the return type of a call of `putStrLn'
| In the expression: putStrLn "yep"
| In a case alternative: (S' Z') -> putStrLn "yep"
| -}
|
|
| Can we reopen the PR with this test? (Distilled from real code I have
| and which fails as of recently.)
|
| Thanks and cheers,
|
| Gabor
|
| On 3/13/13, GHC
participants (1)
-
Simon Peyton-Jones