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 <cvs-ghc@haskell.org> 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
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 <cvs-ghc@haskell.org> 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 | >
On 3/13/13, Simon Peyton-Jones <simonpj@microsoft.com> wrote:
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.
Great, that was the trick! Thanks again, Gabor
Simon
participants (2)
-
Gabor Greif -
Simon Peyton-Jones