#11715: Constraint vs * -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: bug | Status: new Priority: high | Milestone: 8.2.1 Component: Compiler (Type | Version: 8.0.1-rc1 checker) | Resolution: | Keywords: Typeable 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 goldfire): Simon and I recently hit on a possible solution to this long-standing infelicity. 1. Add a new constructor of `RuntimeRep` (of levity-polymorphism fame), `ConstraintRep`. We would then have `type Constraint = TYPE ConstraintRep`. Even though values of types of kind `Constraint` have the same runtime representation as values of types of kind `Type`, it is still OK to have ''more'' distinctions in the type system than are needed at runtime. With this change, we can have things like `Num a -> a` in Core (where there is no distinction between `=>` and `->`), and this would be well- kinded because `->` simply requires that both types have a kind of the form `TYPE blah` for some `blah`. GHC currently desugars one-method (and 0-superclass) classes to be newtypes, not proper datatypes. This is more efficient, of course, than making a new box to store the dictionary. But it means under this new scheme that we have a heterogeneous newtype coercion. For example: {{{#!hs class C a where meth :: a -> a }}} is desugared into {{{#!hs newtype C a = MkCDict { meth :: a -> a } }}} which produces a coercion {{{ axC :: forall (a :: Type). C a ~R# (a -> a) }}} Under our new scheme, this coercion would be heterogeneous, because `C a :: TYPE ConstraintRep` and `(a -> a) :: TYPE LiftedRep`. Of course, GHC (now) handles heterogeneous equalities just fine, but there is a problem: GHC can extract a kind equality from a type equality via its `KindCo` coercion, captured in this typing rule: {{{ co : (t1 :: k1) ~r# (t2 :: k2) ----------------------------------------- KindCo co : (k1 :: Type) ~N# (k2 :: Type) }}} Note that the premise does not require any particular role on the coercion, while the conclusion is always nominal. With `KindCo` (and a few other coercion formers), we could derive a proof of `ConstraintRep ~N# LiftedRep` from `axC`. This is terrible. So: 2. Require the coercion in `KindCo` to be nominal. This makes our equality relation a tiny bit weaker, but I don't think the lost expressiveness will ever bite. GHC does not currently export a heterogeneous version of representational equality (although such a thing exists internally), so users can't every really witness it. And the place where this is key is in decomposing `AppCo`s, but the roles around `AppCo`s mean that the coercion relating the arguments is always nominal. So I think it will work out; building GHC's libraries with this restriction should be an adequate test. One remaining problem is that GHC uses newtype axioms for substitutions in, e.g., newtype unwrapping/normalization. So a heterogeneous axiom is a bad idea. And I'm not yet sure how to fix this. The normal way to avoid heterogeneity is just to cast one side. But we can't do this here, because the coercion we would have to use proves that `Constraint ~N# Type`, which is precisely what we are trying to avoid! So I'm still a bit stuck on this point. Another possible way forward is to do (1), above, and stop encoding one- element classes as newtypes. This has negative performance implications, and so that makes me sad. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11715#comment:47 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler