#16148: Better type inference for Constraint vs Type -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- An enduring infelicity in GHC’s type inference is the treatment of tuples. Consider, this from `RaeJobTalk`: {{{ type family F c sch where F _ '[] = (() :: Constraint) F c (col ': cols) = (c Int, F c cols) }}} When kind-checking `F`, we initially give it a return kind of kappa, a unification variable. Suppose we kind-check the second equation first. Then what kind of tuple is it, a constraint tuple, or an ordinary type tuple. We must unify kappa with `Type` or `Constraint` respectively – and they are different kinds. How can we choose which? Currently we have the following unsatisfactory ruse: 1. Look at the “expected kind”. If we kind-check the second equation first we learn nothing from that 2. Infer kinds for all of the elements of the type. Again in this case we learn nothing. 3. If we still know nothing, arbitrarily pick Type This is horrible. If we kind check the first equation first, step 1 will discover Constraint, and kind checking succeeds. But if we put the equations in the other order, kind checking fails. Ugh! Another example with exactly the same cause is #16139. What to do? I can only think of three approaches: A. Add a pseudo constraint `(TC kappa)` meaning “kappa must eventually turn out to be either `Type` or `Constraint`”. When generalising, default to `Type`. B. Same, but by having a special sort of TauTv, a TCTv, which can only unify with Type or Constraint. Again, do not generalise over such type variables. C. Define {{{ type Type = TYPE (LiftedRep T) type Constraint = TYPE (LiftedRep C) }}} So now we can unify `kappa` with `(TYPE (LiftedRep zeta))` where `zeta` is a unification variable that we must eventually unify with `T` or `C`. Of these, (C) seems most principled, but somehow over-elaborate for our purposes. And the others also seem to be rather too much work to solve a simple, local problem. ------------- For reference, here are the current kinding rules {{{ t1 : TYPE rep1 t2 : TYPE rep2 (FUN) ---------------- t1 -> t2 : Type t1 : Constraint t2 : TYPE rep (PRED1) ---------------- t1 => t2 : Type t1 : Constraint t2 : Constraint (PRED2) --------------------- t1 => t2 : Constraint ty : TYPE rep `a` is not free in rep (FORALL1) ----------------------- forall a. ty : TYPE rep ty : Constraint (FORALL2) ------------------------- forall a. ty : Constraint }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16148 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler