[GHC] #16330: Type inference in presence of pattern matching on GADTs
#16330: Type inference in presence of pattern matching on GADTs -------------------------------------+------------------------------------- Reporter: v0d1ch | Owner: (none) Type: feature | Status: new request | Priority: low | Milestone: Component: Compiler | Version: 8.6.3 Keywords: GADTs | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- This small example {{{ {-# LANGUAGE GADTs #-} data G a where I :: G Integer f g = case g of I -> () }}} yields {{{ • Couldn't match expected type ‘p’ with actual type ‘()’ ‘p’ is untouchable inside the constraints: a ~ Integer bound by a pattern with constructor: I :: G Integer, in a case alternative at gadtsInference.hs:6:17 ‘p’ is a rigid type variable bound by the inferred type of f :: G a -> p at gadtsInference.hs:6:1-23 Possible fix: add a type signature for ‘f’ • In the expression: () In a case alternative: I -> () In the expression: case g of { I -> () } • Relevant bindings include f :: G a -> p (bound at gadtsInference.hs:6:1) | 6 | f g = case g of I -> () | ^^ }}} Without providing the type annotation for f `f :: G a -> ()` GHC cannot infer the correct result type. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16330 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
The key point about GADTs is that pattern matching causes type refinement. For example, in the right hand side of the equation
{{{#!hs eval :: Term a -> a eval (Lit i) = ... }}}
the type `a` is refined to `Int`. That’s the whole point! A precise specification of the type rules is beyond what this user manual aspires to, but the design closely follows that described in the paper [http://research.microsoft.com/%7Esimonpj/papers/gadt/ Simple unification-
#16330: Type inference in presence of pattern matching on GADTs -------------------------------------+------------------------------------- Reporter: v0d1ch | Owner: (none) Type: feature request | Status: closed Priority: low | Milestone: Component: Compiler | Version: 8.6.3 Resolution: invalid | Keywords: GADTs Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => closed * resolution: => invalid Comment: This is expected behavior. Per the [https://downloads.haskell.org/~ghc/8.6.3/docs/html/users_guide/glasgow_exts.... #extension-GADTs users' guide section on GADTs]: based type inference for GADTs], (ICFP 2006). The general principle is this: //type refinement is only carried out based on user-supplied type annotations//. So if no type signature is supplied for eval, no type refinement happens, and lots of obscure error messages will occur. Type inference in the presence of GADT pattern matching is extremely difficult in general (for reasons explained in further detail in the linked paper), and GHC deliberately requires that you supply a type signature to avoid these difficulties. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16330#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC