#10729: Type inference in GADT pattern matches -------------------------------------+------------------------------------- Reporter: mniip | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 7.11 checker) | Resolution: invalid | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Changes (by rwbarton): * status: new => closed * resolution: => invalid Comment: Replying to [ticket:10729 mniip]:
When pattern matching against GADT constructors, GHC seems to have issues with inferring the type of the resulting expression.
Minimal example: Assume the datatype:
{{{ data D a where D :: D () }}} A simple function that pattern matches on it: {{{ a D = () }}} It is expected to have type `D a -> ()`
Why not `a :: D a -> a`? This function definition has no principal type. See the very end of the user's guide section https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/data-type- extensions.html#gadt. The type of the function body is not rigid in your example, because you did not specify it with a type annotation, and the only information about the type comes from inside a pattern match on a refining constructor. It is one of the examples in the linked paper, in appendix A. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10729#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler