Finally nail Constraint vs Type: the plan
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 (closed). Richard and I have spent many, many hours going round in circles on this question.
#11715 (closed) lists tickets that are stuck on this problem. Tickets that relate to this problem
-
#21328 (closed) (
mkFunCo
). Fixed; test intypecheck/should_compile/T21328.hs
-
#11715 (closed). Fixed; tests in
typecheck/should_run/T11715.hs
andindexed-types/should_compile/T11715b.hs
- #11621. Not fixed: tuple syntax
- #12933 (closed)
- #9547. Not fixed: tuple syntax
- #13931 (closed). Not a bug.
-
#15918 (closed) (about
mkCastTy
). Fixed; test inquantified-constraints/T15918.hs
-
#21530 (closed) (ultimately also about
mkCastTy
). Fixed; test intypecheck/should_fail/T21530a
andT21530b
.
"Tuple syntax" means it's about how to interpret "()" in types; this MR and the proposal explicitly to not tackle this.
I have also realised that
- The type-class Specialise pass relies on identifying "dictionary" arguments; that in turn relies on distinguishing
Type
fromConstraint
, in Core. Since the two are (currently) supposed to be equal in Core, that is clearly a pretty dodgy thing to rely on. Notably, the specialiser treats such dictionary args as singleton types. MakingType
andConstraint
completely distinct will help to ensure that we don't accidentally treat a non-singleton type as a singleton type, with potentially disastrous consequences. c.f. #21470 (closed)
This ticket proposes a particular way forward. We invite dicussion. We'll keep this ticket Description up to date with the refined plan.
Related tickets:
-
#22063, #8388, #15979, #19573: return kind of
forall
. - #21229 (closed), #21470 (closed). Specialiser stuff; not really to do with type-vs-constraint.
Update 10 June 2022: this proposal is now a GHC proposal #518 so further discussion should take place there.
We propose to execute as follows:
- Deliver on (2) "The proposal" but make no change under (3) "Newtype classes". That is, adopt "Live with the problem" for newtype classes.
- Consider abolishing newtype classes later.
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
andcoreView
; the latter turnsConstraint
intoType
on the fly. - We have loads of functions that are duplicated (e.g.
tcEqType
andeqType
), and we still get it wrong (e.g.mkCastTy
is used by the type checker but it shouldn't be #15918 (closed)).
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
andCONSTRAINT
(the later is new) are both expressed in terms ofSORT
. -
Type
,Constraint
,TYPE
, andFUN
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 argumentTypeOrConstraint
. We would advertiseSORT
as subject to change; for example we might adopt Kinds are calling conventions. -
Type
andConstraint
are always and everwhere distinct, becuase one hasTypeLike
and one hasConstraintLike
as the first parameter ofSORT
. -
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.
-
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 fromConstraint
; or (more precisely) thatVisible
is not apart fromInvisible
.
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
andConstraint
andVisible
andInvisible
are all allowed in instance heads. It's just thatType
is not apart from constraint (dittoVisible
andInvisible
) so that instance would irretrievably overlap withinstance C (Proxy @Constraint a)
. But this is just the status quo. - Ensure that
-
Abolish newtype classes. There are lots of reasons for doing this: #20897 is the summary ticket, but #21470 (closed), #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
-
If we allow unlifted constraints (such as
(?x :: Int)
), do we need unlifted constraint tuples? What notation should we use for them? -
Do we allow user-written unlifted constraints? What would be the benefits or drawbacks?
5. The kind of forall
Realisation: we have a bunch of tickets about the return type of forall
: #22063, #8388, #15979, #19573.
If we had SORT
we could give it the return type SORT tc rep
, where tc :: TypeOrConstraint
is a unification variable, and is a ConcreteTv. I'm not sure it's worth changing from the TYPE/CON