[Git][ghc/ghc][wip/T24676] Wibbles
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Mon Jun 10 10:13:39 UTC 2024
Simon Peyton Jones pushed to branch wip/T24676 at Glasgow Haskell Compiler / GHC
Commits:
0e7bc76b by Simon Peyton Jones at 2024-06-10T11:11:35+01:00
Wibbles
* Documentation
* Accept simpl017 error message change
- - - - -
3 changed files:
- compiler/GHC/Tc/Gen/App.hs
- compiler/GHC/Tc/Utils/Unify.hs
- testsuite/tests/simplCore/should_compile/simpl017.stderr
Changes:
=====================================
compiler/GHC/Tc/Gen/App.hs
=====================================
@@ -113,7 +113,7 @@ Note [Instantiation variables are short lived]
* An instantation variable is a mutable meta-type-variable, whose level number
is QLInstVar.
-* Ordinary unifcation variables always stand for monotypes; only instantiation
+* Ordinary unification variables always stand for monotypes; only instantiation
variables can be unified with a polytype (by `qlUnify`).
* When we start typechecking the argments of the call, in tcValArgs, we will
@@ -1884,13 +1884,12 @@ foldQLInstVars check_tv ty
qlUnify :: TcType -> TcType -> TcM ()
-- Unify ty1 with ty2:
--- * It unifies /only/ instantiation variables.
--- It does not itself unify ordinary unification variables,
--- although it calls unifyKind which can do so. (It'd be ok for it to
--- unify ordinary unification variables, subject to the usual checks.)
--- * It never produces errors, even for mis-matched types
+-- * It can unify both instantiation variables (possibly with polytypes),
+-- and ordinary unification variables (but only with monotypes)
-- * It does not return a coercion (unlike unifyType); it is called
--- for the sole purpose of unifying instantiation variables
+-- for the sole purpose of unifying instantiation variables, although it
+-- may also (opportunistically) unify regular unification variables.
+-- * It never produces errors, even for mis-matched types
-- * It may return without having made the argument types equal, of course;
-- it just makes best efforts.
qlUnify ty1 ty2
@@ -1899,10 +1898,7 @@ qlUnify ty1 ty2
where
go :: TcType -> TcType
-> TcM ()
- -- The TyVarSets give the variables bound by enclosing foralls
- -- for the corresponding type. Don't unify with these.
go (TyVarTy tv) ty2
--- | isQLInstTyVar tv = go_kappa tv ty2
| isMetaTyVar tv = go_kappa tv ty2
-- Only unify QL instantiation variables
-- See (UQL3) in Note [QuickLook unification]
@@ -1967,7 +1963,6 @@ qlUnify ty1 ty2
-- otherwise we'll fail to unify and emit a coercion.
-- Just an optimisation: emitting a coercion is fine
go_flexi kappa (TyVarTy tv2)
--- | isQLInstTyVar tv2, lhsPriority tv2 > lhsPriority kappa
| lhsPriority tv2 > lhsPriority kappa
= go_flexi1 tv2 (TyVarTy kappa)
go_flexi kappa ty2
@@ -1978,6 +1973,7 @@ qlUnify ty1 ty2
simpleUnifyCheck UC_QuickLook kappa ty2
= do { co <- unifyKind (Just (TypeThing ty2)) ty2_kind kappa_kind
-- unifyKind: see (UQL2) in Note [QuickLook unification]
+ -- and (MIV2) in Note [Monomorphise instantiation variables]
; let ty2' = mkCastTy ty2 co
; traceTc "qlUnify:update" $
ppr kappa <+> text ":=" <+> ppr ty2
@@ -1995,19 +1991,11 @@ In qlUnify, if we find (kappa ~ ty), we are going to update kappa := ty.
That is the entire point of qlUnify! Wrinkles:
(UQL1) Before unifying an instantiation variable in `go_flexi`, we must check
- the usual unification conditions: see `GHC.Tc.Utils.Unify.simpleUnifyCheck`
+ the usual unification conditions, by calling `GHC.Tc.Utils.Unify.simpleUnifyCheck`
In particular:
-
* We must not make an occurs-check; we use occCheckExpand for that.
-
* We must not unify a concrete type variable with a non-concrete type.
-
- `simpleUnifyCheck` also checks for various other things, including
- - foralls; but we specifically *want* to unify foralls here!
- - level mis-match; but instantiation variables are at the innermoest
- level anyway, so this would always succeed
- - type families; relates to a very specific and exotic performance
- question, that is unlikely to bite here
+ * Level mis-match
(UQL2) What if kappa and ty have different kinds? We simply call the
ordinary unifier and use the coercion to connect the two.
@@ -2020,22 +2008,32 @@ That is the entire point of qlUnify! Wrinkles:
BUT: unifyKind has emitted constraint(s) into the Tc monad, so we may as well
use them. (An alternative; use uType directly, if the result is not Refl,
discard the constraints and the coercion, and do not update the instantiation
- variable.)
+ variable. But see "Sadly discarded design alternative" below.)
-(UQL3) qlUnify (and Quick Look generally) is only unifies instantiation
- variables, not regular unification variables. Why? Nothing fundamental.
- ToDo: unfinished
-
- Because instantiation variables don't really have a settled level yet;
+(UQL3) Instantiation variables don't really have a settled level yet;
they have level QLInstVar (see Note [The QLInstVar TcLevel] in GHC.Tc.Utils.TcType.
- So we should be worried that we might unify
+ You might worry that we might unify
alpha[1] := Maybe kappa[qlinst]
and later this kappa turns out to be a level-2 variable, and we have committed
- a skolem-escape error. Boo!
+ a skolem-escape error.
+
+ But happily this can't happen: QL instantiation variables have level infinity,
+ and we never unify a variable with a type from a deeper level.
+
+Sadly discarded design alternative
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+It is very tempting to use `unifyType` rather than `qlUnify`, killing off the
+latter. (Extending `unifyType` slightly to allow it to unify an instantiation
+variable with a polytype is easy.). But I could not see how to make it work:
+
+ * `unifyType` makes the types /equal/, and returns a coercion, and it is hard to
+ marry that up with DeepSubsumption. Absent deep subsumption, this approach
+ might just work.
- Solution: Quick Look only unifies instantiation variables, and the regular
- unifier wont' do this unification because QL instantiation variables have
- level infinity.
+ * I considered making a wrapper for `uType`, which simply discards any deferred
+ equality constraints. But we can't do that: in a heterogeneous equality we might
+ have unified a unification variable (alpha := ty |> co), where `co` is only bound
+ by those constraints.
-}
{- *********************************************************************
=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -2533,12 +2533,16 @@ lhsPriority tv
case tcTyVarDetails tv of
RuntimeUnk -> 0
SkolemTv {} -> 0
- MetaTv { mtv_info = info } -> case info of
- CycleBreakerTv -> 0
- TyVarTv -> 1
- ConcreteTv {} -> 2
- TauTv -> 3
- RuntimeUnkTv -> 4
+ MetaTv { mtv_info = info, mtv_tclvl = lvl }
+ | QLInstVar <- lvl
+ -> 5 -- Eliminate instantiation variables first
+ | otherwise
+ -> case info of
+ CycleBreakerTv -> 0
+ TyVarTv -> 1
+ ConcreteTv {} -> 2
+ TauTv -> 3
+ RuntimeUnkTv -> 4
{- Note [Unification preconditions]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -2908,10 +2912,15 @@ simpleUnifyCheck caller lhs_tv rhs
UC_QuickLook -> isQLInstTyVar lhs_tv
_ -> isRuntimeUnkTyVar lhs_tv
- fam_ok = case caller of
- UC_Solver -> True
- UC_QuickLook -> True
- UC_OnTheFly -> False
+ -- This fam_ok thing relates to a very specific perf problem
+ -- See Note [Prevent unification with type families]
+ -- A couple of QuickLook regression tests rely on unifying with type
+ -- families, so we let it through there (not very principled, but let's
+ -- see if it bites us)
+ fam_ok = case caller of
+ UC_Solver -> True
+ UC_QuickLook -> True
+ UC_OnTheFly -> False
go (TyVarTy tv)
| lhs_tv == tv = False
=====================================
testsuite/tests/simplCore/should_compile/simpl017.stderr
=====================================
@@ -1,25 +1,20 @@
-
-simpl017.hs:55:5: error: [GHC-83865]
- • Couldn't match type: [E m i] -> E' v0 m a
- with: forall v. [E m i] -> E' v m a
- Expected: m (forall v. [E m i] -> E' v m a)
- Actual: m ([E m i] -> E' v0 m a)
- • In a stmt of a 'do' block: return f
+simpl017.hs:55:12: error: [GHC-46956]
+ • Couldn't match type ‘v0’ with ‘v’
+ Expected: [E m i] -> E' v m a
+ Actual: [E m i] -> E' v0 m a
+ because type variable ‘v’ would escape its scope
+ This (rigid, skolem) type variable is bound by
+ a type expected by the context:
+ forall v. [E m i] -> E' v m a
+ at simpl017.hs:55:12
+ • In the first argument of ‘return’, namely ‘f’
+ In a stmt of a 'do' block: return f
In the first argument of ‘E’, namely
‘(do let ix :: [E m i] -> m i
ix [i] = runE i
{-# INLINE f #-}
....
return f)’
- In the expression:
- E (do let ix :: [E m i] -> m i
- ix [i] = runE i
- {-# INLINE f #-}
- ....
- return f)
• Relevant bindings include
f :: [E m i] -> E' v0 m a (bound at simpl017.hs:54:9)
- ix :: [E m i] -> m i (bound at simpl017.hs:52:9)
- a :: arr i a (bound at simpl017.hs:50:11)
- liftArray :: arr i a -> E m (forall v. [E m i] -> E' v m a)
- (bound at simpl017.hs:50:1)
+
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/0e7bc76bd62e2f3eda4b73db1feda9cb370fc3ce
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/0e7bc76bd62e2f3eda4b73db1feda9cb370fc3ce
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/20240610/1af95c4d/attachment-0001.html>
More information about the ghc-commits
mailing list