[Git][ghc/ghc][wip/T16762] Wibbles from Simon
Simon Peyton Jones
gitlab at gitlab.haskell.org
Fri Oct 9 15:01:54 UTC 2020
Simon Peyton Jones pushed to branch wip/T16762 at Glasgow Haskell Compiler / GHC
Commits:
76bbbda7 by Simon Peyton Jones at 2020-10-09T16:01:05+01:00
Wibbles from Simon
- - - - -
5 changed files:
- compiler/GHC/Tc/Errors.hs
- compiler/GHC/Tc/Gen/HsType.hs
- compiler/GHC/Tc/TyCl/PatSyn.hs
- compiler/GHC/Tc/Types/Constraint.hs
- compiler/GHC/Types/Var.hs
Changes:
=====================================
compiler/GHC/Tc/Errors.hs
=====================================
@@ -439,7 +439,12 @@ reportImplic ctxt implic@(Implic { ic_skols = tvs
where
tcl_env = ic_env implic
insoluble = isInsolubleStatus status
- (env1, tvs') = mapAccumL tidyVarBndr (cec_tidy ctxt) tvs
+ (env1, tvs') = mapAccumL tidyVarBndr (cec_tidy ctxt) $
+ scopedSort tvs
+ -- scopedSort: the ic_skols may not be in dependency order
+ -- (see Note [Skolems in an implication] in GHC.Tc.Types.Constraint)
+ -- but tidying goes wrong on out-of-order constraints;
+ -- so we sort them here before tidying
info' = tidySkolemInfo env1 info
implic' = implic { ic_skols = tvs'
, ic_given = map (tidyEvVar env1) given
=====================================
compiler/GHC/Tc/Gen/HsType.hs
=====================================
@@ -4088,6 +4088,7 @@ promotionErr name err
NoDataKindsDC -> text "perhaps you intended to use DataKinds"
PatSynPE -> text "pattern synonyms cannot be promoted"
_ -> text "it is defined and used in the same recursive group"
+ -- RecDataConPE, ClassPE, TyConPE
{-
************************************************************************
=====================================
compiler/GHC/Tc/TyCl/PatSyn.hs
=====================================
@@ -381,16 +381,19 @@ tcCheckPatSynDecl psb at PSB{ psb_id = lname@(L _ name), psb_args = details
univ_tvs = binderVars univ_bndrs
ex_tvs = binderVars ex_bndrs
- -- Skolemise the universals. This is necessary in order to check the actual pattern
- -- type against the expected type. Even though the tyvars in the type are already
- -- skolems, this step changes their TcLevels, avoiding level-check errors when
- -- unifying.
+ -- Skolemise the quantified type variables. This is necessary
+ -- in order to check the actual pattern type against the
+ -- expected type. Even though the tyvars in the type are
+ -- already skolems, this step changes their TcLevels,
+ -- avoiding level-check errors when unifying.
; (skol_subst0, skol_univ_tvs) <- tcInstSkolTyVars univ_tvs
- ; let skol_req_theta = substTheta skol_subst0 req_theta
; (skol_subst, skol_ex_tvs) <- tcInstSkolTyVarsX skol_subst0 ex_tvs
- ; let skol_prov_theta = substTheta skol_subst prov_theta
- skol_arg_tys = substTys skol_subst (map scaledThing arg_tys)
- skol_pat_ty = substTy skol_subst pat_ty
+ ; let skol_univ_bndrs = transferArgFlags univ_bndrs skol_univ_tvs
+ skol_ex_bndrs = transferArgFlags ex_bndrs skol_ex_tvs
+ skol_req_theta = substTheta skol_subst0 req_theta
+ skol_prov_theta = substTheta skol_subst prov_theta
+ skol_arg_tys = substTys skol_subst (map scaledThing arg_tys)
+ skol_pat_ty = substTy skol_subst pat_ty
univ_tv_prs = [ (getName orig_univ_tv, skol_univ_tv)
| (orig_univ_tv, skol_univ_tv) <- univ_tvs `zip` skol_univ_tvs ]
@@ -436,16 +439,6 @@ tcCheckPatSynDecl psb at PSB{ psb_id = lname@(L _ name), psb_args = details
-- Otherwise we may get a type error when typechecking the builder,
-- when that should be impossible
- -- Need to get Specificities right for univ_bndrs
- ; let skol_univ_bndrs = zipWithEqual "tcCheckPatSynDecl"
- xfer_specificity univ_bndrs skol_univ_tvs
- skol_ex_bndrs = zipWithEqual "tcCheckPatSynDecl2"
- xfer_specificity ex_bndrs skol_ex_tvs
-
- xfer_specificity :: VarBndr var Specificity -> TyVar
- -> VarBndr TyVar Specificity
- xfer_specificity bndr tv = mkTyVarBinder (binderArgFlag bndr) tv
-
; traceTc "tcCheckPatSynDecl }" $ ppr name
; tc_patsyn_finish lname dir is_infix lpat'
=====================================
compiler/GHC/Tc/Types/Constraint.hs
=====================================
@@ -1294,14 +1294,30 @@ worrying that 'b' might clash.
Note [Skolems in an implication]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-The skolems in an implication are not there to perform a skolem escape
-check. That happens because all the environment variables are in the
-untouchables, and therefore cannot be unified with anything at all,
-let alone the skolems.
-
-Instead, ic_skols is used only when considering floating a constraint
-outside the implication in GHC.Tc.Solver.floatEqualities or
-GHC.Tc.Solver.approximateImplications
+The skolems in an implication are used:
+
+* When considering floating a constraint outside the implication in
+ GHC.Tc.Solver.floatEqualities or GHC.Tc.Solver.approximateImplications
+ For this, we can treat ic_skols as a set.
+
+* When checking that a /user-specified/ forall (ic_info = ForAllSkol tvs)
+ has its variables in the correct order; see Note [Checking telescopes].
+ Only for these implications does ic_skols need to be a list.
+
+Nota bene: Although ic_skols is a list, it is not necessarily
+in dependency order:
+- In the ic_info=ForAllSkol case, the user might have written them
+ in the wrong order
+- In the case of a type signature like
+ f :: [a] -> [b]
+ the renamer gathers the implicit "outer" forall'd variables {a,b}, but
+ does not know what order to put them in. The type checker can sort them
+ into dependency order, but only after solving all the kind constraints;
+ and to do that it's convenient to create the Implication!
+
+So we accept that ic_skols may be out of order. Think of it as a set or
+(in the case of ic_info=ForAllSkol, a list in user-specified, and possibly
+wrong, order.
Note [Insoluble constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
=====================================
compiler/GHC/Types/Var.hs
=====================================
@@ -79,6 +79,7 @@ module GHC.Types.Var (
isTyVarBinder,
tyVarSpecToBinder, tyVarSpecToBinders, tyVarReqToBinder, tyVarReqToBinders,
mapVarBndr, mapVarBndrs, lookupVarBndr,
+ transferArgFlag, transferArgFlags,
-- ** Constructing TyVar's
mkTyVar, mkTcTyVar,
@@ -657,6 +658,12 @@ tyVarReqToBinders = map tyVarReqToBinder
tyVarReqToBinder :: VarBndr a () -> VarBndr a ArgFlag
tyVarReqToBinder (Bndr tv _) = Bndr tv Required
+transferArgFlag :: VarBndr var1 argf1 -> var2 -> VarBndr var2 argf1
+transferArgFlag (Bndr _ af) v2 = Bndr v2 af
+
+transferArgFlags :: [VarBndr var1 argf1] -> [var2] -> [VarBndr var2 argf1]
+transferArgFlags = zipWithEqual "transferArgFlags" transferArgFlag
+
binderVar :: VarBndr tv argf -> tv
binderVar (Bndr v _) = v
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/76bbbda7e8715e07ec83fcf404af717a97b2ab2d
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/76bbbda7e8715e07ec83fcf404af717a97b2ab2d
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/20201009/732aa561/attachment-0001.html>
More information about the ghc-commits
mailing list