[Git][ghc/ghc][wip/T20666] Comments only
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Fri Dec 23 09:45:48 UTC 2022
Simon Peyton Jones pushed to branch wip/T20666 at Glasgow Haskell Compiler / GHC
Commits:
eb62d802 by Simon Peyton Jones at 2022-12-23T09:45:33+00:00
Comments only
- - - - -
2 changed files:
- compiler/GHC/Tc/TyCl/Instance.hs
- compiler/GHC/Tc/Validity.hs
Changes:
=====================================
compiler/GHC/Tc/TyCl/Instance.hs
=====================================
@@ -1544,8 +1544,8 @@ definition. More precisely:
To achieve the Superclass Invariant, in a dfun definition we can
generate a guaranteed-non-bottom superclass witness from:
(sc1) one of the dictionary arguments itself (all non-bottom)
- (sc2) an immediate superclass of a dictionary that is Paterson-smaller
- than the instance head
+ (sc2) an immediate superclass of a dictionary that is
+ /Paterson-smaller/ than the instance head
See Note [The PatersonSize of a type] in GHC.Tc.Utils.TcType
(sc3) a call of a dfun (always returns a dictionary constructor)
@@ -1567,34 +1567,43 @@ Here is an example, taken from CmmExpr:
(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 is smaller than the thing we are building (UserOfRegs r (Maybe a)).
+For (i1) we can get the (Ord r) superclass by selection from
+(UserOfRegs r a), since it (i.e. UserOfRegs r a) is smaller than the
+thing we are building, namely (UserOfRegs r (Maybe a)).
-But for (i2) that isn't the case, so we must add an explicit, and
-perhaps surprising, (Ord r) argument to the instance declaration.
+But for (i2) that isn't the case: (UserOfRegs r CmmReg) is not smaller
+than the thing we are building (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.
Here's another example from #6161:
- class Super a => Duper a where ...
- class Duper (Fam a) => Foo a where ...
-(i3) instance Foo a => Duper (Fam a) where ...
-(i4) instance Foo Float where ...
+ class Super a => Duper a where ...
+ class Duper (Maybe a) => Foo a where ...
+(i3) instance Foo a => Duper (Maybe a) where ...
+(i4) instance Foo Float where ...
It would be horribly wrong to define
- dfDuperFam :: Foo a -> Duper (Fam a) -- from (i3)
- dfDuperFam d = MkDuper (sc_sel1 (sc_sel2 d)) ...
+ dfDuperMaybe :: Foo a -> Duper (Maybe a) -- from (i3)
+ dfDuperMaybe d = MkDuper (sc_sel1 (sc_sel2 d)) ...
dfFooFloat :: Foo Float -- from (i4)
- dfFooFloat = MkFoo (dfDuperFam dfFooFloat) ...
-
-Now the Super superclass of Duper is definitely bottom!
-
-This won't happen because when processing (i3) we can use the
-superclasses of (Foo a), which is smaller than the head Duper (Fam a).
-This superclass is Duper (Fam a). But that is *not* smaller than the
-head so we can't take *its* superclasses. As a result the program is
-rightly rejected, unless you add (Super (Fam a)) to the context of
-(i3).
+ dfFooFloat = MkFoo (dfDuperMaybe dfFooFloat) ...
+
+Let's expand the RHS of dfFooFloat:
+ dfFooFloat = MkFoo (MkDuper (sc_sel1 (sc_sel2 dfFooFloat)) ...) ...
+That superclass argument to MkDuper is bottom!
+
+This program gets rejected because:
+* When processing (i3) we need to construct a dictionary for Super
+ (Maybe a), to put in the superclass field of (Duper (Maybe a)).
+* We /can/ use the superclasses of (Foo a), because the latter is
+ smaller than the head of the instance, namely Duper (Maybe a).
+* So we know (by (sc2)) that this Duper (Maybe a) dictionary is
+ non-bottom. But because (Duper (Maybe a)) is not smaller than the
+ instance head (Duper (Maybe a)), we can't take *its* superclasses.
+As a result the program is rightly rejected, unless you add
+(Super (Maybe a)) to the context of (i3).
Note [Solving superclass constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
=====================================
compiler/GHC/Tc/Validity.hs
=====================================
@@ -1715,31 +1715,44 @@ The Paterson Conditions ensure termination of instance resolution.
Given an instance declaration
instance (..., C t1.. tn, ...) => D s1 .. sm
-for each class constraint (C t1 ... tn) in the context we check that
+we check that each constraint in the context of the instance is
+"Paterson-smaller" than the instance head. The underlying idea of
+Paterson-smaller is that
-(PC1) No type variable has more occurrences in the constraint than in the head
+ For any ground substitution S, for each constraint P in the
+ context, S(P) has fewer type constructors, counting repetitions,
+ than the head S(H)
-(PC2) The constraint has fewer constructors and variables (taken together and
- counting repetitions) than the head
+More precisely, a constraint P is Paterson-smaller than H iff
-(PC3) The constraint mentions no type functions. A type function
- application can in principle expand to a type of arbitrary size, and
- so are rejected out of hand
+(PC1) No type variable has more (shallow) occurrences in P than in H.
-The underlying idea is that
+ (If not, a substitution that replaces that variable with a big type
+ would make P have many more type constructors than H. Side note: we
+ could in principle skip this test for a variable of kind Bool,
+ since there are no big ground types we can substitute for it.)
- for any ground substitution, each assertion in the
- context has fewer type constructors than the head.
+(PC2) The constraint P has fewer constructors and variables (taken
+ together and counting repetitions) than the head H. This size
+ metric is computed by sizeType.
+
+ (A substitution that replaces each variable with Int demonstrates
+ the need.)
+
+(PC3) The constraint P mentions no type functions.
+
+ (A type function application can in principle expand to a type of
+ arbitrary size, and so are rejected out of hand.)
(See Section 5 of "Understanding functional dependencies via Constraint
Handling Rules", JFP Jan 2007; and the user manual section "Instance
termiantion rules".
We measure "size" with the data type PatersonSize, in GHC.Tc.Utils.TcType.
- data PatersonSize
- = PS_TyFam TyCon
- | PS_Vanilla { ps_tvs :: [TyVar] -- Free tyvars, including repetitions;
- , ps_size :: Int} -- Number of type constructors and variables
+ data PatersonSize
+ = PS_TyFam TyCon
+ | PS_Vanilla { ps_tvs :: [TyVar] -- Free tyvars, including repetitions;
+ , ps_size :: Int} -- Number of type constructors and variables
* ps_tvs deals with (PC1)
* ps_size deals with (PC2)
@@ -2111,10 +2124,10 @@ checkValidAssocTyFamDeflt fam_tc pats =
suggestion = text "The arguments to" <+> quotes (ppr fam_tc)
<+> text "must all be distinct type variables"
--- Make sure that each type family application is
+-- Make sure that each type family application in the RHS is
-- (1) strictly smaller than the lhs,
-- (2) mentions no type variable more often than the lhs, and
--- (3) does not contain any further type family instances.
+-- (3) does not contain any further type family applications
--
checkFamInstRhs :: TyCon -> [Type] -- LHS
-> [(TyCon, [Type])] -- type family calls in RHS
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/eb62d802e3bafa2474ff39ac30a5c5cd69ea9cef
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/eb62d802e3bafa2474ff39ac30a5c5cd69ea9cef
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20221223/84d9ac6a/attachment-0001.html>
More information about the ghc-commits
mailing list