[Git][ghc/ghc][wip/amg/hasfield-2020] 2 commits: Rewrite matchHasField to generate evidence more directly
Adam Gundry
gitlab at gitlab.haskell.org
Wed Sep 16 22:10:26 UTC 2020
Adam Gundry pushed to branch wip/amg/hasfield-2020 at Glasgow Haskell Compiler / GHC
Commits:
2c5a8f22 by Adam Gundry at 2020-09-16T22:39:40+01:00
Rewrite matchHasField to generate evidence more directly
- - - - -
a03af150 by Adam Gundry at 2020-09-16T23:08:51+01:00
Notes and Queries
- - - - -
3 changed files:
- compiler/GHC/Tc/Instance/Class.hs
- compiler/GHC/Tc/TyCl/Utils.hs
- compiler/GHC/Types/FieldLabel.hs
Changes:
=====================================
compiler/GHC/Tc/Instance/Class.hs
=====================================
@@ -44,7 +44,7 @@ import GHC.Core.Class
import GHC.Driver.Session
import GHC.Utils.Outputable
import GHC.Utils.Panic
-import GHC.Utils.Misc( splitAtList, fstOf3 )
+import GHC.Utils.Misc( splitAtList, fstOf3, debugIsOn )
import Data.Maybe
{- *******************************************************************
@@ -606,6 +606,7 @@ matchCoercible args = pprPanic "matchLiftedCoercible" (ppr args)
{-
Note [HasField instances]
~~~~~~~~~~~~~~~~~~~~~~~~~
+
Suppose we have
data T y = MkT { foo :: [y] }
@@ -619,44 +620,56 @@ We want GHC to automatically solve a constraint like
HasField "foo" (T Int) b
-by emitting a new wanted
-
- (T alpha -> ([alpha] -> T alpha, [alpha])) ~# (T Int -> (b -> T Int, b))
+by building a HasField dictionary out of the updater function `$upd:foo:MKT`.
+(See Note [Record updaters] in GHC.Tc.TyCl.Utils for how updaters are built.)
-and building a HasField dictionary out of the updater function `$upd:foo:MKT`.
-See Note [Record updaters] in GHC.Tc.TyCl.Utils for how updaters are built.
+If `foo` is not in scope, or has a higher-rank or existentially
+quantified type, then the constraint is not solved automatically, but
+may be solved by a user-supplied HasField instance. Similarly, if we
+encounter a HasField constraint where the field is not a literal
+string, or does not belong to the type, then we fall back on the
+normal constraint solver behaviour.
-Since HasField is a one-method class, it is represented as a newtype.
-Hence we can solve `HasField "foo" (T Int) b` by taking an expression
-of type `T Int -> (b -> T Int, b)` and casting it using the newtype coercion.
Note that
$upd:foo:MKT :: forall y . T y -> ([y] -> T y, [y])
-so the expression we construct is
+so we instantiate the updater's type with fresh metavariable(s) (here just one,
+namely alpha), emit new wanteds:
+
+ [W] data_co :: T alpha ~# T Int
+ [W] fld_co :: [alpha] ~# b
+
+and construct the dictionary
- $upd:foo:MKT @alpha |> co
+ ev :: HasField "foo" (T Int) b
+ ev = $upd:foo:MKT @alpha |> co
where
co :: (T alpha -> ([alpha] -> T alpha, [alpha])) ~# HasField "foo" (T Int) b
+ co = sym nt_co ; hf_co
-is built from
+ -- From the instantiated newtype coercion, since HasField is a single-method type class
+ nt_co :: HasField "foo" (T alpha) [alpha] ~# (T alpha -> ([alpha] -> T alpha, [alpha]))
- co1 :: (T alpha -> ([alpha] -> T alpha, [alpha])) ~# (T Int -> (b -> T Int, b))
+ hf_co :: HasField "foo" (T alpha) [alpha] ~# HasField "foo" (T Int) b
+ hf_co = HasField <"foo"> data_co fld_co
-which is the new wanted, and
- co2 :: (T Int -> (b -> T Int, b)) ~# HasField "foo" (T Int) b
+Looking at the wanted T alpha ~# T Int, you might think that we could avoid
+instantiating the updater's type with fresh metavariables, and instead construct
+a substitution [Int/alpha] directly. However this would not work for GADTs, for
+example:
-which can be derived from the newtype coercion.
+ data S a where
+ MkS :: { foo :: Either p q } -> S (p,q)
-If `foo` is not in scope, or has a higher-rank or existentially
-quantified type, then the constraint is not solved automatically, but
-may be solved by a user-supplied HasField instance. Similarly, if we
-encounter a HasField constraint where the field is not a literal
-string, or does not belong to the type, then we fall back on the
-normal constraint solver behaviour.
+where the updater's type is
+
+ $upd:foo:MkS :: forall p q. S (p,q) -> (Either p q -> S (p,q), Either p q)
+
+with no direct connection to the parameters of S itself.
-}
-- See Note [HasField instances]
@@ -666,50 +679,81 @@ matchHasField dflags short_cut clas tys
; rdr_env <- getGlobalRdrEnv
; case tys of
-- We are matching HasField {k} x r a...
- [_k_ty, x_ty, r_ty, a_ty]
- -- x should be a literal string
- | Just x <- isStrLitTy x_ty
+ [k, x, r, a]
+ -- x should be a literal string (this implies k is Symbol)
+ | Just x_lit <- isStrLitTy x
-- r should be an applied type constructor
- , Just (tc, args) <- tcSplitTyConApp_maybe r_ty
+ , Just (tc, args) <- tcSplitTyConApp_maybe r
-- use representation tycon (if data family); it has the fields
, let r_tc = fstOf3 (tcLookupDataFamInst fam_inst_envs tc args)
-- x should be a field of r
- , Just fl <- lookupTyConFieldLabel x r_tc
+ , Just fl <- lookupTyConFieldLabel x_lit r_tc
-- the field selector should be in scope
, Just gre <- lookupGRE_FieldLabel rdr_env fl
- -> do { upd_id <- tcLookupId (flUpdate fl)
- ; (tv_prs, preds, upd_ty) <- tcInstType newMetaTyVars upd_id
-
- -- The first new wanted constraint equates the actual
- -- type of the updater with the type (r -> (a -> r, a))
- -- within the HasField x r a dictionary. The preds
- -- will typically be empty, but if the datatype has a
- -- "stupid theta" then we have to include it here.
- ; let theta = mkPrimEqPred upd_ty (mkVisFunTyMany r_ty (mkBoxedTupleTy [mkVisFunTyMany a_ty r_ty, a_ty])) : preds
-
- -- Use the equality proof to cast the updater Id to
- -- type (r -> (a -> r, a)), then use the newtype
- -- coercion to cast it to a HasField dictionary.
- mk_ev (ev1:evs) = evSelector upd_id tvs evs `evCast` co
- where
- co = mkTcSubCo (evTermCoercion (EvExpr ev1))
- `mkTcTransCo` mkTcSymCo co2
- mk_ev [] = panic "matchHasField.mk_ev"
-
- Just (_, co2) = tcInstNewTyCon_maybe (classTyCon clas)
- tys
-
- tvs = mkTyVarTys (map snd tv_prs)
-
+ -> ASSERT ( k `eqType` typeSymbolKind )
+ -- Look up the updater and instantiate its type with fresh metavars
+ do { upd_id <- tcLookupId (flUpdate fl)
+ ; inst_upd@(_, _, upd_ty) <- tcInstType newMetaTyVars upd_id
-- Do not generate an instance if the updater cannot be
-- defined for the field and hence is (). (See Note
-- [Naughty record updaters] in GHC.Tc.TyCl.Utils.)
; if not (upd_ty `eqType` unitTy)
then do { addUsedGRE True gre
- ; return OneInst { cir_new_theta = theta
- , cir_mk_ev = mk_ev
- , cir_what = BuiltinInstance } }
+ ; return $ mkHasFieldEvidence clas (x, r, a)
+ upd_id inst_upd }
else matchInstEnv dflags short_cut clas tys }
_ -> matchInstEnv dflags short_cut clas tys }
+
+-- | Build the dictionary for a @HasField x r a@ constraint using its updater.
+-- See Note [HasField instances].
+mkHasFieldEvidence
+ :: Class -- ^ HasField class
+ -> (Type, Type, Type) -- ^ (x, r, a) type parameters of HasField constraint
+ -> Id -- ^ Updater Id $upd:x:...
+ -> ([(Name, TcTyVar)], TcThetaType, TcType)
+ -- ^ (tyvars, preds, rho) from instantiating the updater's type
+ -> ClsInstResult
+mkHasFieldEvidence clas (x, r, a) upd_id (tv_prs, preds, upd_ty) =
+ OneInst { cir_new_theta = theta
+ , cir_mk_ev = mk_ev
+ , cir_what = BuiltinInstance }
+ where
+ -- Updater types satisfy by construction
+ -- upd_ty = (data_ty -> (fld_ty -> data_ty, fld_ty))
+ -- where data_ty is the datatype and fld_ty is the field type.
+ (_, data_ty, setter_field_pair) = splitFunTy upd_ty
+ (_, [_, fld_ty]) = splitTyConApp setter_field_pair
+
+ -- Emit new wanteds in order to convert `HasField x data_ty fld_ty` (built
+ -- from the updater) into `HasField x r a` (the constraint we are solving).
+ -- The preds will typically be empty, but if the datatype has a "stupid
+ -- theta" it will be included here, as the updater quantifies over it.
+ theta = mkPrimEqPred data_ty r -- data_co :: data_ty ~# r
+ : mkPrimEqPred fld_ty a -- fld_co :: fld_ty ~# a
+ : preds
+
+ -- Instantiate the updater Id appropriately, use the newtype coercion to
+ -- cast it to a `HasField x data_ty fld_ty` dictionary, then use the
+ -- equality witnesses to convert it to a `HasField x r a` dictionary.
+ mk_ev (data_co:fld_co:evs) =
+ evSelector upd_id (mkTyVarTys (map snd tv_prs)) evs
+ `evCast` (mkTcSymCo nt_co `mkTcTransCo` hf_co data_co fld_co)
+ mk_ev evs = pprPanic "mkHasFieldEvidence.mk_ev" (ppr evs)
+
+ -- hf_co :: HasField x data_ty fld_ty ~# HasField x r a
+ -- hf_co = HasField <x> data_co fld_co
+ hf_co data_co fld_co = mkTcTyConAppCo Representational hasFieldTyCon
+ [ mkTcNomReflCo typeSymbolKind
+ , mkTcNomReflCo x
+ , evTermCoercion (EvExpr data_co)
+ , evTermCoercion (EvExpr fld_co)
+ ]
+
+ -- nt_co :: HasField x data_ty fld_ty ~# (data_ty -> (fld_ty -> data_ty, fld_ty))
+ nt_co = maybe (panic "mkHasFieldEvidence:nt_co") snd $
+ tcInstNewTyCon_maybe hasFieldTyCon
+ [typeSymbolKind, x, data_ty, fld_ty]
+
+ hasFieldTyCon = classTyCon clas
=====================================
compiler/GHC/Tc/TyCl/Utils.hs
=====================================
@@ -1183,6 +1183,14 @@ type (e.g. 'b' in T2).
Note the need for casts in the result!
+All this applies to updaters (see Note [Record updaters]) as well as selectors;
+in the example above we will build this updater:
+ $upd:f:T1 :: T [a] -> (Maybe a -> T [a], Maybe a)
+
+If a GADT field has bona-fide existential tyvars that do not appear in the
+result type, the selector will be naughty (see Note [Naughty record selectors]).
+
+
Note [Selector running example]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
It's OK to combine GADTs and type families. Here's a running example:
@@ -1268,7 +1276,7 @@ Note that:
scope.
* The Name of each updater is stored alongside that of the selector in the
- 'FieldLabel's in each 'DataCon'.
+ 'FieldLabel's in each 'DataCon'. See the notes in GHC.Types.FieldLabel.
* Renamed-syntax bindings for both a selector and an updater for each field are
produced by mkRecordSelectorAndUpdater; these bindings are then type-checked
@@ -1285,6 +1293,16 @@ Note that:
name to () instead, even if we can generate the corresponding selector. See
Note [Naughty record updaters].
+ * We could imagine generating the selector *from* the updater, i.e. build
+ $sel:foo:T r = case $upd:foo:T r of (_, x) -> x
+ but we don't do so because the updater might be naughty, and for pattern
+ synonyms will not exist at all (see Note [No updaters for pattern synonyms]).
+
+ * For GADTs, we insist that all constructors mentioning a field have the same
+ type, and reject the definition entirely if not. Thus if the field does not
+ involve an existential (and hence is not naughty) we can make both a selector
+ and an updater (see Note [GADT record selectors]).
+
Note [Naughty record updaters]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1332,7 +1350,9 @@ do this at HasField constraint solving time instead, at least for updaters?
Note [No updaters for pattern synonyms]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
For record pattern synonyms, we generate a selector function, but not an
-updater. The updater function is not necessary because we do not solve HasField
+updater. In principle it would be possible to build an updater for
+bidirectional pattern synonyms, but not for unidirectional ones. In any case,
+the updater function is not necessary because we do not solve HasField
constraints for fields defined by pattern synonyms.
That is, given
@@ -1355,10 +1375,11 @@ which will be subject to the usual rules around orphan instances and the
restrictions on when HasField instances can be defined (as described in
Note [Validity checking of HasField instances] in GHC.Tc.Validity).
-We could imagine allowing record pattern synonyms to lead to automatic HasField
-constraint solving, but this potentially introduces incoherent HasField
-instances, because multiple pattern synonyms (in different modules) might use
-the same field name in the same type, and would even lead to e.g.
+We could imagine allowing (bidirectional) record pattern synonyms to lead to
+automatic HasField constraint solving, but this potentially introduces
+incoherent HasField instances, because multiple pattern synonyms (in different
+modules) might use the same field name in the same type, and would even lead to
+e.g.
pattern Id{id} = id
=====================================
compiler/GHC/Types/FieldLabel.hs
=====================================
@@ -40,6 +40,11 @@ Now there will be two FieldLabel values for 'foo', one in T and one in
U. They share the same label (FieldLabelString), but the selector
functions differ.
+There is no Deep and Subtle Reason why we couldn't use mangled $sel: names for
+all selectors, not just those defined when DuplicateRecordFields is enabled.
+However, this exposes various bugs in the DuplicateRecordFields implementation,
+so we have not yet made this simplification.
+
See also Note [Representing fields in AvailInfo] in GHC.Types.Avail.
Note [Why selector names include data constructors]
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/fdff0fe1834729148842ac0d7b94e68a9c916466...a03af1504b3cb178a070f58a2afefa681ad37f07
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/fdff0fe1834729148842ac0d7b94e68a9c916466...a03af1504b3cb178a070f58a2afefa681ad37f07
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/20200916/c8400666/attachment-0001.html>
More information about the ghc-commits
mailing list