[Git][ghc/ghc][wip/T23051] 2 commits: Wibbles

Simon Peyton Jones (@simonpj) gitlab at gitlab.haskell.org
Tue Mar 7 11:56:57 UTC 2023



Simon Peyton Jones pushed to branch wip/T23051 at Glasgow Haskell Compiler / GHC


Commits:
b9038e9f by Simon Peyton Jones at 2023-03-07T11:39:13+00:00
Wibbles

Tricky!

- - - - -
1b10277a by Simon Peyton Jones at 2023-03-07T11:58:09+00:00
More wibbles

- - - - -


2 changed files:

- compiler/GHC/Tc/Solver.hs
- compiler/GHC/Tc/Utils/TcMType.hs


Changes:

=====================================
compiler/GHC/Tc/Solver.hs
=====================================
@@ -1559,7 +1559,7 @@ and we are running simplifyInfer over
 
 These are two implication constraints, both of which contain a
 wanted for the class C. Neither constraint mentions the bound
-skolem. We might imagine that these constraint could thus float
+skolem. We might imagine that these constraints could thus float
 out of their implications and then interact, causing beta1 to unify
 with beta2, but constraints do not currently float out of implications.
 
@@ -1695,12 +1695,11 @@ decideMonoTyVars :: InferMode
 --   (a) Mentioned in a constraint we can't generalise (the MR)
 --   (b) Mentioned in the kind of a CoVar; we can't quantify over a CoVar,
 --       so we must not quantify over a type variable free in its kind
---   (c) Free in the kind of the type(s) we are generalising
---   (d) Connected by an equality or fundep to
+--   (c) Connected by an equality or fundep to
 --          * a type variable at level < N, or
 --          * A tyvar subject to (a), (b) or (c)
 -- Having found all such level-N tyvars that we can't generalise,
--- promote them, to elimianate them from further consideration
+-- promote them, to eliminate them from further consideration
 --
 -- Also return CoVars that appear free in the final quantified types
 --   we can't quantify over these, and we must make sure they are in scope
@@ -1720,11 +1719,7 @@ decideMonoTyVars infer_mode name_taus psigs candidates
        ; tc_lvl <- TcM.getTcLevel
        ; let psig_tys = mkTyVarTys psig_qtvs ++ psig_theta
 
-             -- (b) kind_vars are the variables free in the kinds of the taus
-             kind_vars = foldr (unionVarSet . tyCoVarsOfType . typeKind)
-                               emptyVarSet taus
-
-             -- (c) The co_var_tvs are tvs mentioned in the types of covars or
+             -- (b) The co_var_tvs are tvs mentioned in the types of covars or
              -- coercion holes. We can't quantify over these covars, so we
              -- must include the variable in their types in the mono_tvs.
              -- E.g.  If we can't quantify over co :: k~Type, then we can't
@@ -1747,7 +1742,6 @@ decideMonoTyVars infer_mode name_taus psigs candidates
                -- typecheck/should_compile/tc213
 
              mono_tvs1 = mono_tvs0 `unionVarSet` co_var_tvs
-                                   `unionVarSet` kind_vars
 
                -- mono_tvs1 is now the set of variables from an outer scope
                -- (that's mono_tvs0) and the set of covars, closed over kinds.
@@ -1830,40 +1824,32 @@ decideMonoTyVars infer_mode name_taus psigs candidates
 defaultTyVarsAndSimplify :: TcLevel
                          -> [PredType]          -- Assumed zonked
                          -> TcM [PredType]      -- Guaranteed zonked
--- Promote the known-monomorphic tyvars;
 -- Default any tyvar free in the constraints;
 -- and re-simplify in case the defaulting allows further simplification
 defaultTyVarsAndSimplify rhs_tclvl candidates
   = do {  -- Default any kind/levity vars
        ; DV {dv_kvs = cand_kvs, dv_tvs = cand_tvs}
                 <- candidateQTyVarsOfTypes candidates
-                -- decideMonoTyVars has promoted any type variable fixed by the
-                --   type envt, so they won't be chosen by candidateQTyVarsOfTypes
-                -- Any covars should already be handled by
-                -- the logic in decideMonoTyVars, which looks at
-                -- the constraints generated
+         -- NB1: decideMonoTyVars has promoted any type variable fixed by the
+         --      type envt, so they won't be chosen by candidateQTyVarsOfTypes
+         -- NB2: Defaulting for variables free in tau_tys is done later, by quantifyTyVars
+         --      Hence looking only at 'candidates'
+         -- NB3: Any covars should already be handled by
+         --      the logic in decideMonoTyVars, which looks at
+         --      the constraints generated
 
        ; poly_kinds  <- xoptM LangExt.PolyKinds
-       ; mapM_ (default_one poly_kinds True) (dVarSetElems cand_kvs)
-       ; mapM_ (default_one poly_kinds False) (dVarSetElems (cand_tvs `minusDVarSet` cand_kvs))
+       ; let default_kv | poly_kinds = defaultTyVar DefaultKindVars
+                        | otherwise  = default_tv
+             default_tv = defaultTyVar (NonStandardDefaulting DefaultNonStandardTyVars)
+       ; mapM_ default_kv (dVarSetElems cand_kvs)
+       ; mapM_ default_tv (dVarSetElems (cand_tvs `minusDVarSet` cand_kvs))
 
        ; simplify_cand candidates
        }
   where
-    default_one poly_kinds is_kind_var tv
-      | not (isMetaTyVar tv)
-      = return ()
-      | otherwise
-      = void $ defaultTyVar
-          (if not poly_kinds && is_kind_var
-           then DefaultKindVars
-           else NonStandardDefaulting DefaultNonStandardTyVars)
-          -- NB: only pass 'DefaultKindVars' when we know we're dealing with a kind variable.
-          tv
-
-       -- this common case (no inferred constraints) should be fast
-    simplify_cand [] = return []
-       -- see Note [Unconditionally resimplify constraints when quantifying]
+    -- See Note [Unconditionally resimplify constraints when quantifying]
+    simplify_cand [] = return []  -- Fast path
     simplify_cand candidates
       = do { clone_wanteds <- newWanteds DefaultOrigin candidates
            ; WC { wc_simple = simples } <- setTcLevel rhs_tclvl $


=====================================
compiler/GHC/Tc/Utils/TcMType.hs
=====================================
@@ -45,8 +45,6 @@ module GHC.Tc.Utils.TcMType (
   unpackCoercionHole, unpackCoercionHole_maybe,
   checkCoercionHole,
 
-  ConcreteHole, newConcreteHole,
-
   newImplication,
 
   --------------------------------
@@ -414,23 +412,6 @@ checkCoercionHole cv co
              | otherwise
              = False
 
--- | A coercion hole used to store evidence for `Concrete#` constraints.
---
--- See Note [The Concrete mechanism].
-type ConcreteHole = CoercionHole
-
--- | Create a new (initially unfilled) coercion hole,
--- to hold evidence for a @'Concrete#' (ty :: ki)@ constraint.
-newConcreteHole :: Kind -- ^ Kind of the thing we want to ensure is concrete (e.g. 'runtimeRepTy')
-                -> Type -- ^ Thing we want to ensure is concrete (e.g. some 'RuntimeRep')
-                -> TcM (ConcreteHole, TcType)
-                  -- ^ where to put the evidence, and a metavariable to store
-                  -- the concrete type
-newConcreteHole ki ty
-  = do { concrete_ty <- newFlexiTyVarTy ki
-       ; let co_ty = mkHeteroPrimEqPred ki ki ty concrete_ty
-       ; hole <- newCoercionHole co_ty
-       ; return (hole, concrete_ty) }
 
 {- **********************************************************************
 *
@@ -1467,9 +1448,6 @@ collect_cand_qtvs orig_ty is_dep cur_lvl bound dvs ty
 --                     _                -> False
 --                -> return dv  -- Skip inner skolems; ToDo: explain
 
-      | isConcreteTyVar tv
-      = return dv  -- Never quantify over a "concrete" meta-tyvar (#23051)
-
       | tv `elemDVarSet` kvs
       = return dv  -- We have met this tyvar already
 
@@ -1825,17 +1803,27 @@ defaultTyVar def_strat tv
   = do { traceTc "Defaulting a RuntimeRep var to LiftedRep" (ppr tv)
        ; writeMetaTyVar tv liftedRepTy
        ; return True }
+
   | isLevityVar tv
   , default_ns_vars
   = do { traceTc "Defaulting a Levity var to Lifted" (ppr tv)
        ; writeMetaTyVar tv liftedDataConTy
        ; return True }
+
   | isMultiplicityVar tv
   , default_ns_vars
   = do { traceTc "Defaulting a Multiplicity var to Many" (ppr tv)
        ; writeMetaTyVar tv manyDataConTy
        ; return True }
 
+  | isConcreteTyVar tv
+    -- We don't want to quantify; but neither can we default to anything
+    -- sensible.  So we just promote.  Not very satisfing, but it's very
+    -- much a corner case: #23051
+  = do { lvl <- getTcLevel
+       ; _ <- promoteMetaTyVarTo lvl tv
+       ; return True }
+
   | DefaultKindVars <- def_strat -- -XNoPolyKinds and this is a kind var: we must default it
   = default_kind_var tv
 
@@ -1980,7 +1968,7 @@ What do do?
  D. We could error.
 
 We choose (D), as described in #17567, and implement this choice in
-doNotQuantifyTyVars.  Discussion of alternativs A-C is below.
+doNotQuantifyTyVars.  Discussion of alternatives A-C is below.
 
 NB: this is all rather similar to, but sadly not the same as
     Note [Naughty quantification candidates]



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/386fbabc7f453bc23327d6f7e474d973aa0ef06e...1b10277a03196fbea62f2ca90106402c031f186c

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/386fbabc7f453bc23327d6f7e474d973aa0ef06e...1b10277a03196fbea62f2ca90106402c031f186c
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/20230307/fc10030f/attachment-0001.html>


More information about the ghc-commits mailing list