diff options
author | Richard Eisenberg <rae@richarde.dev> | 2021-11-22 17:34:32 -0500 |
---|---|---|
committer | Simon Peyton Jones <simon.peytonjones@gmail.com> | 2023-01-11 08:30:42 +0000 |
commit | aed1974e92366ab8e117734f308505684f70cddf (patch) | |
tree | bbfe7fdd00f1e0ef8dacdcf8d070a07efa38561b /docs | |
parent | 083f701553852c4460159cd6deb2515d3373714d (diff) | |
download | haskell-aed1974e92366ab8e117734f308505684f70cddf.tar.gz |
Refactor the treatment of loopy superclass dictswip/T20666
This patch completely re-engineers how we deal with loopy superclass
dictionaries in instance declarations. It fixes #20666 and #19690
The highlights are
* Recognise that the loopy-superclass business should use precisely
the Paterson conditions. This is much much nicer. See
Note [Recursive superclasses] in GHC.Tc.TyCl.Instance
* With that in mind, define "Paterson-smaller" in
Note [Paterson conditions] in GHC.Tc.Validity, and the new
data type `PatersonSize` in GHC.Tc.Utils.TcType, along with
functions to compute and compare PatsonSizes
* Use the new PatersonSize stuff when solving superclass constraints
See Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance
* In GHC.Tc.Solver.Monad.lookupInInerts, add a missing call to
prohibitedSuperClassSolve. This was the original cause of #20666.
* Treat (TypeError "stuff") as having PatersonSize zero. See
Note [Paterson size for type family applications] in GHC.Tc.Utils.TcType.
* Treat the head of a Wanted quantified constraint in the same way
as the superclass of an instance decl; this is what fixes #19690.
See GHC.Tc.Solver.Canonical Note [Solving a Wanted forall-constraint]
(Thanks to Matthew Craven for this insight.)
This entailed refactoring the GivenSc constructor of CtOrigin a bit,
to say whether it comes from an instance decl or quantified constraint.
* Some refactoring way in which redundant constraints are reported; we
don't want to complain about the extra, apparently-redundant
constraints that we must add to an instance decl because of the
loopy-superclass thing. I moved some work from GHC.Tc.Errors to
GHC.Tc.Solver.
* Add a new section to the user manual to describe the loopy
superclass issue and what rules it follows.
Diffstat (limited to 'docs')
-rw-r--r-- | docs/users_guide/exts/instances.rst | 104 |
1 files changed, 94 insertions, 10 deletions
diff --git a/docs/users_guide/exts/instances.rst b/docs/users_guide/exts/instances.rst index 7776a7f833..84276527a3 100644 --- a/docs/users_guide/exts/instances.rst +++ b/docs/users_guide/exts/instances.rst @@ -180,18 +180,10 @@ syntactically allowed. Some further various observations about this grammar: .. _instance-rules: .. _instance-termination: -.. _undecidable-instances: Instance termination rules ~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. extension:: UndecidableInstances - :shortdesc: Enable undecidable instances. - - :since: 6.8.1 - - Permit definition of instances which may lead to type-checker non-termination. - Regardless of :extension:`FlexibleInstances` and :extension:`FlexibleContexts`, instance declarations must conform to some rules that ensure that instance resolution will terminate. The restrictions can be lifted with @@ -212,6 +204,9 @@ The rules are these: application can in principle expand to a type of arbitrary size, and so are rejected out of hand + If these three conditions hold we say that the constraint ``(C t1 ... tn)`` is + **Paterson-smaller** than the instance head. + 2. The Coverage Condition. For each functional dependency, ⟨tvs⟩\ :sub:`left` ``->`` ⟨tvs⟩\ :sub:`right`, of the class, every type variable in S(⟨tvs⟩\ :sub:`right`) must appear in @@ -318,10 +313,99 @@ indeed the (somewhat strange) definition: makes instance inference go into a loop, because it requires the constraint ``(Mul a [b] b)``. -The :extension:`UndecidableInstances` extension is also used to lift some of the -restrictions imposed on type family instances. See +.. _undecidable-instances: + +Undecidable instances and loopy superclasses +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +.. extension:: UndecidableInstances + :shortdesc: Enable undecidable instances. + + :since: 6.8.1 + + Permit definition of instances which may lead to type-checker non-termination. + +The :extension:`UndecidableInstances` extension lifts the restrictions on +on instance declarations described in :ref:`instance-termination`. +The :extension:`UndecidableInstances` extension also lifts some of the +restrictions imposed on type family instances; see :ref:`type-family-decidability`. + +With :extension:`UndecidableInstances` it is possible to create a superclass cycle, +which leads to the program failing to terminate. To avoid this, GHC imposes +rules on the way in which superclass constraints are satisfied in an instance +declaration. These rules apply even when :extension:`UndecidableInstances` is enabled. +Consider:: + + class C a => D a where ... + + instance Wombat [b] => D [b] where ... + +When typechecking this ``instance`` declaration, GHC must ensure that ``D``'s superclass, +``(C [b])`` is satisfied. We say that ``(C [b])`` is a **Wanted superclass constraint** of the +instance declaration. + +If there is an ``instance blah => C [b]``, which is often the +case, GHC can use the instance declaration and all is well. But suppose there is no +such instance, so GHC can only satisfy the Wanted ``(C [b])`` from the context of the instance, +namely the Given constraint ``(Wombat [b])``. Perhaps the declaration of ``Wombat`` looks like this:: + + class C a => Wombat a + +So the Given ``(Wombat [b])`` has a superclass ``(C [b])``, and it looks as if we can satisfy the +Wanted ``(C [b])`` constraint from this superclass of ``Wombat``. But it turns out that +allowing this can lead to subtle looping dictionaries, and GHC prevents it. + +The rule is this: **a Wanted superclass constraint can only be satisfied in one of these three ways:** + +.. rst-class:: open + +1. *Directly from the context of the instance declaration*. For example, if the declaration looked like this:: + + instance (Wombat [b], C [b]) => D [b] where ... + + we could satisfy the Wanted ``(C [b])`` from the Given ``(C [b])``. + +2. *Using another instance declaration*. For example, if we had:: + + instance C b => C [b] where ... + + we can satisfy the Wanted superclass constraint ``(C [b])`` using this instance, + reducing it to the Wanted constraint ``(C b)`` (which still has to be solved). + +3. *Using the immediate superclass of a Given constraint X that is Paterson-smaller than the head of the instance declaration.* + The rules for Paterson-smaller are precisely those described in :ref:`instance-rules`: + + - No type variable can occur more often in X than in the instance head. + + - X must have fewer type constructors and variables (taken together and counting repetitions) than the instance head. + + - X must mention no type functions. + +Rule (3) is the tricky one. Here is an example, taken from GHC's own source code:: + + class Ord r => UserOfRegs r a where ... + (i1) instance UserOfRegs r a => UserOfRegs r (Maybe a) where + (i2) instance (Ord r, UserOfRegs r CmmReg) => UserOfRegs r CmmExpr where + +For ``(i1)`` we can get the ``(Ord r)`` superclass by selection from +``(UserOfRegs r a)``, since it (i.e. ``UserOfRegs r a``) is Paterson-smaller than the +head of the instance declaration, namely ``(UserOfRegs r (Maybe a))``. + +But for ``(i2)`` that isn't the case: ``(UserOfRegs r CmmReg)`` is not Paterson-smaller +than the head of the instance ``(UserOfRegs r CmmExpr)``, so we can't use +the superclasses of the former. Hence we must instead add an explicit, +and perhaps surprising, ``(Ord r)`` argument to the instance declaration. + +This fix, of simply adding an apparently-redundant constraint to the context +of an instance declaration, is robust: it always fixes the problem. +(We considered adding it automatically, but decided that it was better be explicit.) + +Fixing this subtle superclass cycle has a long history; if you are interested, read +``Note [Recursive superclasses]`` and ``Note [Solving superclass constraints]`` +in ``GHC.Tc.TyCl.Instance``. + .. _instance-overlap: Overlapping instances |