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 wrote: | > #7766: equality constraints exposed by patterns mess up constraint | > inference | > ----------------------------------------+----------------------------- | > ----------------------------------------+------ | > Reporter: heisenbug | Owner: | > Type: bug | Status: closed | > Priority: normal | Milestone: | > Component: Compiler | Version: 7.7 | > Resolution: invalid | Keywords: | > Os: Unknown/Multiple | Architecture: | Unknown/Multiple | > Failure: GHC rejects valid program | Difficulty: Unknown | > Testcase: | Blockedby: | > Blocking: | Related: | > ----------------------------------------+----------------------------- | > ----------------------------------------+------ | > Changes (by simonpj): | > | > * status: new => closed | > * difficulty: => Unknown | > * resolution: => invalid | > | > | > Comment: | > | > This is by design. Type inference in the presence of GADTs is | tricky! | > | > If you give the signature `main :: IO ()` it works fine. But here | > you are asking GHC to ''infer'' the type of `main`. (Remember, | > Haskell doesn't insist on `IO ()`; the `main` function can have type | > `IO Char`.) | > | > Becuase you are pattern matching against GADTs there are equalities | > in scope, so GHC declines to contrain the type of `main`. In this | > particular case there is only one answer, but that's very hard to | > figure out, so we fail conservatively. | > | > Bottom line: use type signatures when pattern matching on GADTs. | > | > Simon | > | > -- | > Ticket URL: | > http://hackage.haskell.org/trac/ghc/ticket/7766#comment:1 | > GHC http://www.haskell.org/ghc/ | > The Glasgow Haskell Compiler | >