[Git][ghc/ghc][wip/T24676] More fixes:
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Wed May 15 10:55:43 UTC 2024
Simon Peyton Jones pushed to branch wip/T24676 at Glasgow Haskell Compiler / GHC
Commits:
fc00c883 by Simon Peyton Jones at 2024-05-15T11:54:22+01:00
More fixes:
Not fully documented yet
* Recall: the danger is of unifying an inscope regular unification variable
alpha[n] := (...kappa[n]...), where kappa is an instantiation variable, and then
subsequently demote kappa[n].
* Remove unifyType from instantiateSigma (unnecessary, very seldom fires)
* Remove unifyKind from qlUnify. Rationale:
* The whole point of qlUnify is to get (kappa := ∀a. blah). If we get
(kappa := (∀ a. blah) ▷ co) there is no point whatsoever.
* So we can use qlUnify on the kinds, and check that we get tcEqType.
* I also realised that in the IVAR rule we should add all the fresh variables to delta.
* Net result: no calls of unifyType in QuickLook
- - - - -
2 changed files:
- compiler/GHC/Tc/Gen/App.hs
- compiler/GHC/Tc/Utils/Instantiate.hs
Changes:
=====================================
compiler/GHC/Tc/Gen/App.hs
=====================================
@@ -639,7 +639,7 @@ tcInstFun do_ql inst_final fun_ctxt tc_fun fun_sigma rn_args
| fun_is_out_of_scope, looks_like_type_arg arg -- See Note [VTA for out-of-scope functions]
= go delta acc so_far fun_ty rest_args
- -- Rule IALL from Fig 4 of the QL paper
+ -- Rule IALL from Fig 4 of the QL paper; applies even if args = []
-- Instantiate invisible foralls and dictionaries.
-- c.f. GHC.Tc.Utils.Instantiate.topInstantiate
go1 delta acc so_far fun_ty args
@@ -720,37 +720,24 @@ tcInstFun do_ql inst_final fun_ctxt tc_fun fun_sigma rn_args
-- - We need the freshly allocated unification variables, to extend
-- delta with.
-- It's easier just to do the job directly here.
- do { let val_args = leadingValArgs args
- val_args_count = length val_args
-
- -- Create metavariables for the arguments. Following matchActualFunTy,
- -- we create nu_i :: TYPE kappa_i[conc], ensuring that the arguments
- -- have concrete runtime representations.
- -- When we come to unify the nus (in qlUnify), we will call
- -- unifyKind on the kinds. This will do the right thing, even though
- -- we are manually filling in the nu metavariables.
- new_arg_tv (L _ arg) i =
- newOpenFlexiFRRTyVar $
- FRRExpectedFunTy (ExpectedFunTyArg (HsExprTcThing tc_fun) arg) i
- ; arg_nus <- zipWithM new_arg_tv
- val_args
- [length so_far + 1 ..]
- -- We need variables for multiplicity (#18731)
- -- Otherwise, 'undefined x' wouldn't be linear in x
- ; mults <- replicateM val_args_count (newFlexiTyVarTy multiplicityTy)
- ; res_nu <- newOpenFlexiTyVar
+ do { arg_tys <- zipWithM new_arg_ty (leadingValArgs args) [length so_far + 1 ..]
+ ; res_ty <- newOpenFlexiTyVarTy
+ ; let fun_ty' = mkScaledFunTys arg_tys res_ty
+ delta' = delta `unionVarSet` tyCoVarsOfType fun_ty'
+ -- All the fresh variables belong in delta'
+
+ -- Fill in kappa := nu_1 -> .. -> nu_n -> res_nu
+ -- NB: kappa is uninstantiated ('go' already checked that)
; kind_co <- unifyKind Nothing liftedTypeKind (tyVarKind kappa)
- ; let delta' = delta `extendVarSetList` (res_nu:arg_nus)
- arg_tys = mkTyVarTys arg_nus
- res_ty = mkTyVarTy res_nu
- fun_ty' = mkScaledFunTys (zipWithEqual "tcInstFun" mkScaled mults arg_tys) res_ty
- co_wrap = mkWpCastN (mkGReflLeftCo Nominal fun_ty' kind_co)
+ -- unifyKind: see (UQL1) in Note [Actual unification during QuickLook]
+ ; liftZonkM (writeMetaTyVar kappa (mkCastTy fun_ty' kind_co))
+
+ ; let co_wrap = mkWpCastN (mkGReflLeftCo Nominal fun_ty' kind_co)
acc' = addArgWrap co_wrap acc
-- Suppose kappa :: kk
-- Then fun_ty :: kk, fun_ty' :: Type, kind_co :: Type ~ kk
-- co_wrap :: (fun_ty' |> kind_co) ~ fun_ty'
- ; liftZonkM $ writeMetaTyVar kappa (mkCastTy fun_ty' kind_co)
- -- kappa is uninstantiated ('go' already checked that)
+
; go delta' acc' so_far fun_ty' args }
-- Rule IARG from Fig 4 of the QL paper:
@@ -778,6 +765,20 @@ tcInstFun do_ql inst_final fun_ctxt tc_fun fun_sigma rn_args
; let acc' = arg' : addArgWrap wrap acc
; go delta' acc' (arg_ty:so_far) res_ty rest_args }
+ new_arg_ty :: LHsExpr GhcRn -> Int -> TcM (Scaled TcType)
+ -- Make a fresh nus for each argument in rule IVAR
+ new_arg_ty (L _ arg) i
+ = do { arg_nu <- newOpenFlexiFRRTyVarTy $
+ FRRExpectedFunTy (ExpectedFunTyArg (HsExprTcThing tc_fun) arg) i
+ -- Following matchActualFunTy, we create nu_i :: TYPE kappa_i[conc],
+ -- thereby ensuring that the arguments have concrete runtime representations
+
+ ; mult_ty <- newFlexiTyVarTy multiplicityTy
+ -- mult_ty: e need variables for argument multiplicities (#18731)
+ -- Otherwise, 'undefined x' wouldn't be linear in x
+
+ ; return (mkScaled mult_ty arg_nu) }
+
-- Is the argument supposed to instantiate a forall?
--
-- In other words, given a function application `fn arg`,
@@ -1871,29 +1872,38 @@ qlUnify delta ty1 ty2
----------------
go_flexi (_,bvs2) kappa ty2 -- ty2 is zonked
- | -- See Note [Actual unification in qlUnify]
+ | -- See Note [Actual unification during QuickLook]
let ty2_tvs = shallowTyCoVarsOfType ty2
, not (ty2_tvs `intersectsVarSet` bvs2)
- -- Can't instantiate a delta-varto a forall-bound variable
+ -- Can't instantiate a delta-var to a forall-bound variable
, Just ty2 <- occCheckExpand [kappa] ty2
-- Passes the occurs check
- = do { let ty2_kind = typeKind ty2
- kappa_kind = tyVarKind kappa
- ; co <- unifyKind (Just (TypeThing ty2)) ty2_kind kappa_kind
- -- unifyKind: see Note [Actual unification in qlUnify]
-
- ; traceTc "qlUnify:update" $
- vcat [ hang (ppr kappa <+> dcolon <+> ppr kappa_kind)
- 2 (text ":=" <+> ppr ty2 <+> dcolon <+> ppr ty2_kind)
- , text "co:" <+> ppr co ]
- ; liftZonkM $ writeMetaTyVar kappa (mkCastTy ty2 co) }
+ , not (isConcreteTyVar kappa) || isConcreteType ty2
+ -- Don't unify a concrete instantiatiation variable with a non-concrete type
+ = do { let kappa_kind = tyVarKind kappa
+ ty2_kind = typeKind ty2
+ ; kinds_ok <- go_kinds kappa_kind ty2_kind
+ ; when kinds_ok $
+ do { traceTc "qlUnify:update" $
+ hang (ppr kappa <+> dcolon <+> ppr kappa_kind)
+ 2 (text ":=" <+> ppr ty2 <+> dcolon <+> ppr ty2_kind)
+ ; liftZonkM $ writeMetaTyVar kappa ty2 }}
| otherwise
= return () -- Occurs-check or forall-bound variable
+ go_kinds :: TcKind -> TcKind -> TcM Bool
+ go_kinds kind1 kind2
+ | kind1 `tcEqType` kind2 = return True
+ | otherwise = do { qlUnify delta kind1 kind2
+ ; liftZonkM $
+ do { kind1 <- zonkTcType kind1
+ ; kind2 <- zonkTcType kind2
+ ; return (kind1 `tcEqType` kind2) } }
-{- Note [Actual unification in qlUnify]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+{- Note [Actual unification during QuickLook]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In qlUnify, if we find (kappa ~ ty), we are going to update kappa := ty.
That is the entire point of qlUnify! Wrinkles:
@@ -1930,6 +1940,9 @@ That is the entire point of qlUnify! Wrinkles:
because it doesn't unify polykinds, and has all kinds of other
magic. qlUnify is very focused.
+Wrinkles
+(UQL1) .. todo ...
+
TL;DR Calling unifyKind seems like the lesser evil.
-}
=====================================
compiler/GHC/Tc/Utils/Instantiate.hs
=====================================
@@ -329,9 +329,11 @@ instCallConstraints orig preds
| null preds
= return idHsWrapper
| otherwise
- = do { evs <- mapM go preds
+ = do { evs <- mapM (emitWanted orig) preds
; traceTc "instCallConstraints" (ppr evs)
; return (mkWpEvApps evs) }
+{-
+-- ToDo: explain why we don't short-cut here; Quick Look
where
go :: TcPredType -> TcM EvTerm
go pred
@@ -347,6 +349,7 @@ instCallConstraints orig preds
| otherwise
= emitWanted orig pred
+-}
instDFunType :: DFunId -> [DFunInstType]
-> TcM ( [TcType] -- instantiated argument types
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/fc00c88393a8d0f0d3453597ae6cfbbd52229994
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/fc00c88393a8d0f0d3453597ae6cfbbd52229994
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/20240515/2f9ff3ed/attachment-0001.html>
More information about the ghc-commits
mailing list