GitLab

For well over 5 years we have struggled with the fact that Constraint and Type are considered distinct by the typechecker, but the same in Core. This strange behaviour has led to a raft of troubling issues, which are summarised in #11715. Richard and I have spent many, many hours going round in circles on this question.

#11715 lists tickets that are stuck on this problem.

This ticket proposes a particular way forward. We invite dicussion. We'll keep this ticket Description up to date with the refined plan.

Update 10 June 2022: this proposal is now a GHC proposal #518 so further discussion should take place there.

---

1. The problem

In GHC today, Constraint and Type are

• distinct in the typechecker
• equal in Core

This leads to a lot of duplication, with subtle distinctions between the duplicates. For example:

• We have two functions tcView and coreView; the latter turns Constraint into Type on the fly.
• We have loads of functions that are duplicated (e.g. tcEqType and eqType), and we still get it wrong (e.g. mkCastTy is used by the type checker but it shouldn't be #15918).

We created this situation because we thought it was a small wart; but it has proved to be a very painful and recurrent wart, and one we want to fix.

---

2. The proposal

We propose the following type structure:

type SORT :: TypeOrConstraint -> RuntimeRep -> Type

data TypeOrConstraint = TypeLike | ConstraintLike

type TYPE       = SORT TypeLike        :: RuntimeRep -> Type
type CONSTRAINT = SORT ConstraintLike  :: RuntimeRep -> Type
type Type       = TYPE       LiftedRep :: Type
type Constraint = CONSTRAINT LiftedRep :: Type

type (->) = FUN Many

type FUN   :: forall (m::Multiplicity) (rr1 :: RuntimeRep) (rr2 :: RuntimeRep).
                              TYPE rr1       -> TYPErr2        -> Type
type (=>)  :: forall rr1 rr2. CONSTRAINT rr1 -> TYPE       rr2 -> Type
type (==>) :: forall rr1 rr2. CONSTRAINT rr1 -> CONSTRAINT rr2 -> Constraint

The key points are

• TYPE and CONSTRAINT (the later is new) are both expressed in terms of SORT.

• Type, Constraint, TYPE, and FUN all have the same kinds as today, and we would expect that stability to continue into the future.

• A new type constructor SORT has an argument TypeOrConstraint. We would advertise SORT as subject to change; for example we might adopt Kinds are calling conventions.

• Type and Constraint are always and everwhere distinct, becuase one has TypeLike and one has ConstraintLike as the first parameter of SORT.

• There are three arrow type constructors, instead of one. (NB: FUN exists today.)

• Notice that FUN is multiplicity-polymorphic, while (=>) and (==>) are not. We don't want multiplicity polymorphism on fat arrows.

• This plan naturally supports unlifted constraints, such as

  (?x :: Int#) :: TYPE Invisible IntRep

  It is tempting to lump (~#) as an unlifted constraint, but (~#) is inhabited by coercions, not terms, and so doing so is likely to be more misleading than clarifying.

Naming conventions aside, this proposal is entirely about internal matters, so we do not propose to write a GHC proposal.

2.1 The naming of cats

An alternative would be to continue with TYPE as the fundamental type constructor, like this:

type TYPE :: TypeOrConstraint -> RuntimeRep -> Type

type Type       = TYPE TypeLike       LiftedRep :: Type
type Type#      = TYPE TypeLike                 :: RuntimeRep -> Type
type Constraint = TYPE ConstraintLike LiftedRep :: Type

But this disruption would be unpopular.

2.2 Tuples

This proposal does not address the problem of tuples, although is tempting to do so. Currently we have:

(,)   :: Type -> Type -> Type
(%,%) :: Constraint -> Constraint -> Constraint

except that the latter is written, in source Haskell, as (c1,c2). That leads to syntactic ambiguity. If I write:

type S a b a = ((a,b), c)

do I intend to define a Constraint synonym, or a Type synonym? It's tempting to give (,) a polymorphic type

(,) :: forall (v:VisCo). TYPE v LiftedRep -> TYPE v LiftedRep -> Type v LiftedRep

But, tempting as it is, we do not propose this. The tuples problem is all about concrete syntax. It just so happens that we use the same parentheses and commas for normal tuples and constraint tuples. No one has asked for polymorphism here. And it seems overwrought to complexify our type system just to allow for this little concrete-syntax convenience. Letting tuple syntax drive the type system is the tail wagging the dog.

2.3 Implementation notes

Inside GHC we do not propose to change the representation of types:

data Type = ...
  | FunTy { ft_af   :: AnonArgFlag    -- Is this (->), or (=>)/(==>)?
          , ft_mult :: Mult           -- Multiplicity
          , ft_arg  :: Type           -- Argument type
          , ft_res  :: Type }         -- Result type

The splitTyConApp_maybe function would have to consult the kind of ft_arg and ft_res to decide which function arrow TyCon to return. A Type would be ill-kinded if ft_arg and ft_res do not have SORT tc rr where tc is either TypeLike or ConstraintLike (but nothing else). Incidentally the ft_af flag is just a cache for whether ft_arg has kind TypeLike or ConsraintLike -- this is true today.

3. Newtype classes

There is a difficulty with newtype classes. Consider

class C a where { op :: a -> a }

If we implemented the class as a newtype, as we do today, we'd have an axiom

C_ax :: (C a) ~ (a->a)

But KindCo (which extracts a coercion among kinds from a coercion among types) would yield

   KindCo C_ax :: Constraint ~ Type

If Constraint and Type are distinct, that looks like a contradiction, and who knows what kind of chaos can result.

There are two possible ways forward here.

1. Live with the problem. You might worry that from Constraint ~ Type we could deduce anything at all; but that is not so in GHC. The most worrying possibility is this:

   type instance F Type = Int
   type instance F Constraint = Bool

   And now we can create a coercion Int ~ F Type ~ F Constraint ~ Bool. And that really would be bad. But we can defeat this plan by the following simple expedient (which GHC adopts already, today):

   • Ensure that Type is not apart from Constraint; or (more precisely) that Visible is not apart from Invisible.

   That in turn means that the above type instance declarations are rejected as overlapping.

   This is the situation in GHC today, so "live with the problem" makes nothing worse.

   Note that nothing prevents writing instances like e.g. instance C (Proxy @Type a). In particular, Type and Constraint and Visible and Invisible are all allowed in instance heads. It's just that Type is not apart from constraint (ditto Visible and Invisible) so that instance would irretrievably overlap with instance C (Proxy @Constraint a). But this is just the status quo.

2. Abolish newtype classes. There are lots of reasons for doing this: #20897 is the summary ticket, but #21470, #21229 (closed), #21328 (closed) are also relevant. This is probably the better solution, but it's not on the critical path.

4. Further extensions

The plan could be elaborated to make more distinctions. We do not propose to adopt these extensions now; we just sketch them.

4.1 Incoherent classes

Ordinary type classes are coherent; there is only one value of type (Eq [Int]) for example. Put another way, class constraints are singleton types. But implicit parameters are different: there are many values of type ?x :: Int. We say they are incoherent. We could express this distinction in the kind system:

data VisCoh = Visible | Invisible Coherence
data Coherence = Coherent | Incoherent

type IP :: forall rr. Symbol -> Type# rr -> TYPE (Invisible Incoherent) rr

Incoherent constraints are treated specially:

• Incoherent constraints cannot appear in the superclasses of a coherent class declaration
• Incoherent constraints cannot appear in the context of a coherent instance declaration
• The type-class Specialiser only specialises on coherent constraints
• The "short-cut solver" solves only coherent constraints; see Note [Shortcut solving] in GHC.Tc.Solver.Interact

(NB: This notion of incoherence is all about what values inhabit a type. It is notionally distinct from -XIncoherentInstances, which is all about type inference.)

At the moment, all these situations are dealt with by explicitly checking for the class IP; using the kinds would be more systematic. Moreover, the current system can be tricked. E.g.

instance c => C c Int where ...

Suppose the solver is confronted with the Wanted constraint [W] C (?x::Int) Int. It may well use the instance declaration. But then that is very like having an instance declaration with an implicit parameter in the context, which we do not allow, for good reasons. We want to say "c ranges only over coherent constraints", and the kinds let us do that.

Moreover, we could allow the user to declare a class as Incoherent, thus

type InCoh :: Type -> TYPE (Invisible Incoherent) LiftedRep
class Incoh a where ...

Now it entirely OK to use withDict on that class, even without a singleton type argument. (This otherwise risks incoherence; see #21575.)

Under this plan, we could inline withDict, because it would no longer need special treatment.

4.2 Singleton types

One could go further:

data VisCoh = Visible Coherence | Invisible Coherence

and give singleton types a kind TYPE (Visible Coherent) rep, and ordinary value types the kind TYPE (Visible Incoherent) rep.

This would have some nice properties -- e.g. withDict could insist on singleton types -- but it would carry heavy costs. For example:

  Just :: forall (coh:Coherence) (a :: TYPE (Visible coh) LiftedRep). a -> Mabye @coh a

Loads of functions end up becoming coherence-polymorphic, which add a lot of clutter.

Moreover, we don't have a good way to infer (or even reliably check) singleton-type-hood.

4.3 Coherence polymorphism

We don't sketch this out in any detail, but it would be plausible to have coherence polymorphism in arrow types, but the complexity budget is well exhausted by now.

4.4 Other open questions

1. If we allow unlifted constraints (such as (?x :: Int)), do we need unlifted constraint tuples? What notation should we use for them?

2. Do we allow user-written unlifted constraints? What would be the benefits or drawbacks?

6. Steps in the plan

We propose to execute as follows:

1. Deliver on (2) "The proposal" but make no change under (3) "Newtype classes". That is, adopt "Live with the problem" for newtype classes.
2. Consider abolishing newtype classes later.