#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 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Richard responds: This has come up before, of course. I've always had an affinity for choice (A). It's easy to describe, even to users, and I think it will lead to nice error messages (which can special-case printing unsolved TC constraints). I don't think it would take all that much code. (C) doesn't actually work, tempting though it may be. Consider ( {{{ f :: forall (r :: RuntimeRep) (a :: TYPE r). a -> () }}} Don't worry about levity-polymorphism restrictions in binding positions, as that's not the issue here. The question is: does f take 1 visible argument or 0? The answer depends on the choice of r (under plan C), because r might be LiftedRep C. So have no way of reliably instantiating f's type at an occurrence and are thus dead in the water. Plan D: {{{ data TC = T | C TYPE :: RuntimeRep -> TC -> Type }}} That is, make the T/C distinction totally orthogonal to representation, and simply disallow any quantification over a type whose kind has a variable in the TC position. This has the nice side effect of allowing unlifted constraints (e.g., an unboxed implicit parameter or a strict dictionary). But it has the significant drawback of polluting the type of `(->)`, which would now be {{{ (->) :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep) (tc1 :: TC) (tc2 :: TC). TYPE r1 tc1 -> TYPE r2 tc2 -> TYPE LiftedRep tc2 }}} Indeed, we have considered this route before, [https://github.com/ghc- proposals/ghc- proposals/blob/0506dd68fefa26f56dd8e377d4c9d34bf241252f/proposals/0000 -constraint-vs-type.rst here]. The main drawback I see from that abandoned approach in the proposal is that it banned newtype-classes. I don't think we have a satisfactory way (yet) of eliminating newtype-classes while keeping, e.g., reflection working. (This matters: singletons uses the reflection trick to change exponentially-slow processes to linear ones.) Summing up, I see two ways forward: - Simon's (A) - (D) above, including banning newtype-classes and coming up with a new way for the reflection trick to work. Simon's (B) would work, but it seems strictly inferior to (A), simply because a new TyVar flavor is a more obscure approach to getting the behavior we would see in (A), whereas (A) uses an abstraction (a class- like constraint) that everyone knows and loves. Between these two approaches, (A) is at least an order of magnitude easier. So I vote for that. :) I do believe, though, that we'll have to do (D) eventually, though. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16148#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler