#10729: Type inference in GADT pattern matches -------------------------------------+------------------------------------- Reporter: mniip | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.11 (Type checker) | Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: GHC rejects Unknown/Multiple | valid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Revisions: | -------------------------------------+------------------------------------- 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 -> ()` (Note: not `D () -> ()`, existence of a `D` should ensure `()`, not the type signature), but instead it errors: {{{ error: Couldn't match expected type ‘t’ with actual type ‘()’ ‘t’ is untouchable inside the constraints: t1 ~ () bound by a pattern with constructor: D :: D (), in an equation for ‘a’ ‘t’ is a rigid type variable bound by the inferred type of a :: D t1 -> t }}} Note that the error goes away when we annotate the type of the function: {{{ b :: D a -> () -- no error b D = () }}} Or if we supply another branch that clarifies the type: {{{ c D = () -- no error c _ = () }}} But it reappears if the other branch doesn't provide anything to infer from: {{{ d D = () -- error d _ = undefined }}} The same issue happens in `case`: {{{ e x = case x of D -> () -- error }}} But only when the value being matched comes from outside: {{{ f = case D of D -> () -- no error }}} This behavior is reprooducible and identical in 7.8.4. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10729 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler