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-...@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 > _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs