diff options
| author | Simon Peyton Jones <simonpj@microsoft.com> | 2017-12-21 13:31:13 +0000 |
|---|---|---|
| committer | Simon Peyton Jones <simonpj@microsoft.com> | 2017-12-21 14:14:21 +0000 |
| commit | a492af06d3264530d134584f22ffb726a16c78ec (patch) | |
| tree | 294b0c21775d6a7cb9b79c86145d7b6ca47c81ea | |
| parent | 72938f5890dac81afad52bf58175c1e29ffbc6dd (diff) | |
| download | haskell-a492af06d3264530d134584f22ffb726a16c78ec.tar.gz | |
Refactor coercion holes
In fixing Trac #14584 I found that it would be /much/ more
convenient if a "hole" in a coercion (much like a unification
variable in a type) acutally had a CoVar associated with it
rather than just a Unique. Then I can ask what the free variables
of a coercion is, and get a set of CoVars including those
as-yet-un-filled in holes.
Once that is done, it makes no sense to stuff coercion holes
inside UnivCo. They were there before so we could know the
kind and role of a "hole" coercion, but once there is a CoVar
we can get that info from the CoVar. So I removed HoleProv
from UnivCoProvenance and added HoleCo to Coercion.
In summary:
* Add HoleCo to Coercion and remove HoleProv from UnivCoProvanance
* Similarly in IfaceCoercion
* Make CoercionHole have a CoVar in it, not a Unique
* Make tyCoVarsOfCo return the free coercion-hole variables
as well as the ordinary free CoVars. Similarly, remember
to zonk the CoVar in a CoercionHole
We could go further, and remove CoercionHole as a distinct type
altogther, just collapsing it into HoleCo. But I have not done
that yet.
25 files changed, 234 insertions, 208 deletions
diff --git a/compiler/backpack/RnModIface.hs b/compiler/backpack/RnModIface.hs index 2199965d13..c52fce772d 100644 --- a/compiler/backpack/RnModIface.hs +++ b/compiler/backpack/RnModIface.hs @@ -654,6 +654,7 @@ rnIfaceCo (IfaceForAllCo bndr co1 co2) = IfaceForAllCo <$> rnIfaceTvBndr bndr <*> rnIfaceCo co1 <*> rnIfaceCo co2 rnIfaceCo (IfaceFreeCoVar c) = pure (IfaceFreeCoVar c) rnIfaceCo (IfaceCoVarCo lcl) = IfaceCoVarCo <$> pure lcl +rnIfaceCo (IfaceHoleCo lcl) = IfaceHoleCo <$> pure lcl rnIfaceCo (IfaceAxiomInstCo n i cs) = IfaceAxiomInstCo <$> rnIfaceGlobal n <*> pure i <*> mapM rnIfaceCo cs rnIfaceCo (IfaceUnivCo s r t1 t2) diff --git a/compiler/coreSyn/CoreFVs.hs b/compiler/coreSyn/CoreFVs.hs index 4855c1749a..7fcff90c71 100644 --- a/compiler/coreSyn/CoreFVs.hs +++ b/compiler/coreSyn/CoreFVs.hs @@ -386,13 +386,13 @@ orphNamesOfCo (CoherenceCo co1 co2) = orphNamesOfCo co1 `unionNameSet` orphNames orphNamesOfCo (KindCo co) = orphNamesOfCo co orphNamesOfCo (SubCo co) = orphNamesOfCo co orphNamesOfCo (AxiomRuleCo _ cs) = orphNamesOfCos cs +orphNamesOfCo (HoleCo _) = emptyNameSet orphNamesOfProv :: UnivCoProvenance -> NameSet orphNamesOfProv UnsafeCoerceProv = emptyNameSet orphNamesOfProv (PhantomProv co) = orphNamesOfCo co orphNamesOfProv (ProofIrrelProv co) = orphNamesOfCo co orphNamesOfProv (PluginProv _) = emptyNameSet -orphNamesOfProv (HoleProv _) = emptyNameSet orphNamesOfCos :: [Coercion] -> NameSet orphNamesOfCos = orphNamesOfThings orphNamesOfCo diff --git a/compiler/coreSyn/CoreLint.hs b/compiler/coreSyn/CoreLint.hs index 7f52dbbc9e..17fa980ec3 100644 --- a/compiler/coreSyn/CoreLint.hs +++ b/compiler/coreSyn/CoreLint.hs @@ -1666,8 +1666,6 @@ lintCoercion co@(UnivCo prov r ty1 ty2) ; check_kinds kco k1 k2 } PluginProv _ -> return () -- no extra checks - HoleProv h -> addErrL $ - text "Unfilled coercion hole:" <+> ppr h ; when (r /= Phantom && classifiesTypeWithValues k1 && classifiesTypeWithValues k2) @@ -1874,6 +1872,11 @@ lintCoercion this@(AxiomRuleCo co cs) [ text "Expected:" <+> int (n + length es) , text "Provided:" <+> int n ] +lintCoercion (HoleCo h) + = do { addErrL $ text "Unfilled coercion hole:" <+> ppr h + ; lintCoercion (CoVarCo (coHoleCoVar h)) } + + ---------- lintUnliftedCoVar :: CoVar -> LintM () lintUnliftedCoVar cv diff --git a/compiler/iface/IfaceSyn.hs b/compiler/iface/IfaceSyn.hs index ed96d33826..ac988c26d0 100644 --- a/compiler/iface/IfaceSyn.hs +++ b/compiler/iface/IfaceSyn.hs @@ -1434,8 +1434,8 @@ freeNamesIfCoercion (IfaceAppCo c1 c2) freeNamesIfCoercion (IfaceForAllCo _ kind_co co) = freeNamesIfCoercion kind_co &&& freeNamesIfCoercion co freeNamesIfCoercion (IfaceFreeCoVar _) = emptyNameSet -freeNamesIfCoercion (IfaceCoVarCo _) - = emptyNameSet +freeNamesIfCoercion (IfaceCoVarCo _) = emptyNameSet +freeNamesIfCoercion (IfaceHoleCo _) = emptyNameSet freeNamesIfCoercion (IfaceAxiomInstCo ax _ cos) = unitNameSet ax &&& fnList freeNamesIfCoercion cos freeNamesIfCoercion (IfaceUnivCo p _ t1 t2) @@ -1465,7 +1465,6 @@ freeNamesIfProv IfaceUnsafeCoerceProv = emptyNameSet freeNamesIfProv (IfacePhantomProv co) = freeNamesIfCoercion co freeNamesIfProv (IfaceProofIrrelProv co) = freeNamesIfCoercion co freeNamesIfProv (IfacePluginProv _) = emptyNameSet -freeNamesIfProv (IfaceHoleProv _) = emptyNameSet freeNamesIfTyVarBndr :: TyVarBndr IfaceTvBndr vis -> NameSet freeNamesIfTyVarBndr (TvBndr tv _) = freeNamesIfTvBndr tv diff --git a/compiler/iface/IfaceType.hs b/compiler/iface/IfaceType.hs index 41120da4d3..c5a4a3d6db 100644 --- a/compiler/iface/IfaceType.hs +++ b/compiler/iface/IfaceType.hs @@ -196,8 +196,8 @@ data IfaceTyConSort = IfaceNormalTyCon -- ^ a regular tycon {- Note [Free tyvars in IfaceType] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Nowadays (since Nov 16, 2016) we pretty-print a Type by converting to an -IfaceType and pretty printing that. This eliminates a lot of +Nowadays (since Nov 16, 2016) we pretty-print a Type by converting to +an IfaceType and pretty printing that. This eliminates a lot of pretty-print duplication, and it matches what we do with pretty-printing TyThings. @@ -255,7 +255,6 @@ data IfaceCoercion | IfaceTyConAppCo Role IfaceTyCon [IfaceCoercion] | IfaceAppCo IfaceCoercion IfaceCoercion | IfaceForAllCo IfaceTvBndr IfaceCoercion IfaceCoercion - | IfaceFreeCoVar CoVar -- See Note [Free tyvars in IfaceType] | IfaceCoVarCo IfLclName | IfaceAxiomInstCo IfExtName BranchIndex [IfaceCoercion] | IfaceUnivCo IfaceUnivCoProv Role IfaceType IfaceType @@ -268,29 +267,26 @@ data IfaceCoercion | IfaceKindCo IfaceCoercion | IfaceSubCo IfaceCoercion | IfaceAxiomRuleCo IfLclName [IfaceCoercion] + | IfaceFreeCoVar CoVar -- See Note [Free tyvars in IfaceType] + | IfaceHoleCo CoVar -- ^ See Note [Holes in IfaceCoercion] data IfaceUnivCoProv = IfaceUnsafeCoerceProv | IfacePhantomProv IfaceCoercion | IfaceProofIrrelProv IfaceCoercion | IfacePluginProv String - | IfaceHoleProv Unique - -- ^ See Note [Holes in IfaceUnivCoProv] -{- -Note [Holes in IfaceUnivCoProv] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -When typechecking fails the typechecker will produce a HoleProv UnivCoProv to -stand in place of the unproven assertion. While we generally don't want to let -these unproven assertions leak into interface files, we still need to be able to -pretty-print them as we use IfaceType's pretty-printer to render Types. For this -reason IfaceUnivCoProv has a IfaceHoleProv constructor; however, we fails when -asked to serialize to a IfaceHoleProv to ensure that they don't end up in an -interface file. To avoid an import loop between IfaceType and TyCoRep we only -keep the hole's Unique, since that is all we need to print. --} +{- Note [Holes in IfaceCoercion] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +When typechecking fails the typechecker will produce a HoleCo to stand +in place of the unproven assertion. While we generally don't want to +let these unproven assertions leak into interface files, we still need +to be able to pretty-print them as we use IfaceType's pretty-printer +to render Types. For this reason IfaceCoercion has a IfaceHoleCo +constructor; however, we fails when asked to serialize to a +IfaceHoleCo to ensure that they don't end up in an interface file. + -{- %************************************************************************ %* * Functions over IFaceTypes @@ -419,6 +415,7 @@ substIfaceType env ty go_co (IfaceForAllCo {}) = pprPanic "substIfaceCoercion" (ppr ty) go_co (IfaceFreeCoVar cv) = IfaceFreeCoVar cv go_co (IfaceCoVarCo cv) = IfaceCoVarCo cv + go_co (IfaceHoleCo cv) = IfaceHoleCo cv go_co (IfaceAxiomInstCo a i cos) = IfaceAxiomInstCo a i (go_cos cos) go_co (IfaceUnivCo prov r t1 t2) = IfaceUnivCo (go_prov prov) r (go t1) (go t2) go_co (IfaceSymCo co) = IfaceSymCo (go_co co) @@ -437,7 +434,6 @@ substIfaceType env ty go_prov (IfacePhantomProv co) = IfacePhantomProv (go_co co) go_prov (IfaceProofIrrelProv co) = IfaceProofIrrelProv (go_co co) go_prov (IfacePluginProv str) = IfacePluginProv str - go_prov (IfaceHoleProv h) = IfaceHoleProv h substIfaceTcArgs :: IfaceTySubst -> IfaceTcArgs -> IfaceTcArgs substIfaceTcArgs env args @@ -1077,19 +1073,17 @@ ppr_co ctxt_prec co@(IfaceForAllCo {}) = let (tvs, co'') = split_co co' in ((name,kind_co):tvs,co'') split_co co' = ([], co') --- Why these two? See Note [TcTyVars in IfaceType] -ppr_co _ (IfaceFreeCoVar covar) = ppr covar -ppr_co _ (IfaceCoVarCo covar) = ppr covar +-- Why these three? See Note [TcTyVars in IfaceType] +ppr_co _ (IfaceFreeCoVar covar) = ppr covar +ppr_co _ (IfaceCoVarCo covar) = ppr covar +ppr_co _ (IfaceHoleCo covar) = braces (ppr covar) ppr_co ctxt_prec (IfaceUnivCo IfaceUnsafeCoerceProv r ty1 ty2) = maybeParen ctxt_prec TyConPrec $ text "UnsafeCo" <+> ppr r <+> pprParendIfaceType ty1 <+> pprParendIfaceType ty2 -ppr_co _ctxt_prec (IfaceUnivCo (IfaceHoleProv u) _ _ _) - = braces $ ppr u - -ppr_co _ (IfaceUnivCo _ _ ty1 ty2) +ppr_co _ (IfaceUnivCo _ _ ty1 ty2) = angleBrackets ( ppr ty1 <> comma <+> ppr ty2 ) ppr_co ctxt_prec (IfaceInstCo co ty) @@ -1358,8 +1352,6 @@ instance Binary IfaceCoercion where put_ bh a put_ bh b put_ bh c - put_ _ (IfaceFreeCoVar cv) - = pprPanic "Can't serialise IfaceFreeCoVar" (ppr cv) put_ bh (IfaceCoVarCo a) = do putByte bh 6 put_ bh a @@ -1407,6 +1399,11 @@ instance Binary IfaceCoercion where putByte bh 17 put_ bh a put_ bh b + put_ _ (IfaceFreeCoVar cv) + = pprPanic "Can't serialise IfaceFreeCoVar" (ppr cv) + put_ _ (IfaceHoleCo cv) + = pprPanic "Can't serialise IfaceHoleCo" (ppr cv) + -- See Note [Holes in IfaceUnivCoProv] get bh = do tag <- getByte bh @@ -1477,9 +1474,6 @@ instance Binary IfaceUnivCoProv where put_ bh (IfacePluginProv a) = do putByte bh 4 put_ bh a - put_ _ (IfaceHoleProv _) = - pprPanic "Binary(IfaceUnivCoProv) hit a hole" empty - -- See Note [Holes in IfaceUnivCoProv] get bh = do tag <- getByte bh diff --git a/compiler/iface/TcIface.hs b/compiler/iface/TcIface.hs index 1a2d737726..6fad8da87c 100644 --- a/compiler/iface/TcIface.hs +++ b/compiler/iface/TcIface.hs @@ -1341,7 +1341,6 @@ tcIfaceCo = go go (IfaceForAllCo tv k c) = do { k' <- go k ; bindIfaceTyVar tv $ \ tv' -> ForAllCo tv' k' <$> go c } - go (IfaceFreeCoVar c) = pprPanic "tcIfaceCo:IfaceFreeCoVar" (ppr c) go (IfaceCoVarCo n) = CoVarCo <$> go_var n go (IfaceAxiomInstCo n i cs) = AxiomInstCo <$> tcIfaceCoAxiom n <*> pure i <*> mapM go cs go (IfaceUnivCo p r t1 t2) = UnivCo <$> tcIfaceUnivCoProv p <*> pure r @@ -1359,6 +1358,8 @@ tcIfaceCo = go go (IfaceSubCo c) = SubCo <$> go c go (IfaceAxiomRuleCo ax cos) = AxiomRuleCo <$> go_axiom_rule ax <*> mapM go cos + go (IfaceFreeCoVar c) = pprPanic "tcIfaceCo:IfaceFreeCoVar" (ppr c) + go (IfaceHoleCo c) = pprPanic "tcIfaceCo:IfaceHoleCo" (ppr c) go_var :: FastString -> IfL CoVar go_var = tcIfaceLclId @@ -1374,8 +1375,6 @@ tcIfaceUnivCoProv IfaceUnsafeCoerceProv = return UnsafeCoerceProv tcIfaceUnivCoProv (IfacePhantomProv kco) = PhantomProv <$> tcIfaceCo kco tcIfaceUnivCoProv (IfaceProofIrrelProv kco) = ProofIrrelProv <$> tcIfaceCo kco tcIfaceUnivCoProv (IfacePluginProv str) = return $ PluginProv str -tcIfaceUnivCoProv (IfaceHoleProv _) = - pprPanic "tcIfaceUnivCoProv" (text "holes can't occur in interface files") {- ************************************************************************ diff --git a/compiler/iface/ToIface.hs b/compiler/iface/ToIface.hs index e28abdfe41..deb84ca694 100644 --- a/compiler/iface/ToIface.hs +++ b/compiler/iface/ToIface.hs @@ -218,7 +218,9 @@ toIfaceCoercionX fr co go (CoVarCo cv) -- See [TcTyVars in IfaceType] in IfaceType | cv `elemVarSet` fr = IfaceFreeCoVar cv - | otherwise = IfaceCoVarCo (toIfaceCoVar cv) + | otherwise = IfaceCoVarCo (toIfaceCoVar cv) + go (HoleCo h) = IfaceHoleCo (coHoleCoVar h) + go (AppCo co1 co2) = IfaceAppCo (go co1) (go co2) go (SymCo co) = IfaceSymCo (go co) go (TransCo co1 co2) = IfaceTransCo (go co1) (go co2) @@ -250,7 +252,6 @@ toIfaceCoercionX fr co go_prov (PhantomProv co) = IfacePhantomProv (go co) go_prov (ProofIrrelProv co) = IfaceProofIrrelProv (go co) go_prov (PluginProv str) = IfacePluginProv str - go_prov (HoleProv h) = IfaceHoleProv (chUnique h) toIfaceTcArgs :: TyCon -> [Type] -> IfaceTcArgs toIfaceTcArgs = toIfaceTcArgsX emptyVarSet diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs index 1785b8be48..907f31b65a 100644 --- a/compiler/typecheck/TcCanonical.hs +++ b/compiler/typecheck/TcCanonical.hs @@ -172,7 +172,7 @@ solveCallStack ev ev_cs = do -- dictionary, so we have to coerce ev_cs to a dictionary for -- `IP ip CallStack`. See Note [Overview of implicit CallStacks] let ev_tm = mkEvCast (EvCallStack ev_cs) (wrapIP (ctEvPred ev)) - setWantedEvBind (ctEvId ev) ev_tm + setWantedEvBind (ctEvEvId ev) ev_tm canClass :: CtEvidence -> Class -> [Type] diff --git a/compiler/typecheck/TcEnv.hs b/compiler/typecheck/TcEnv.hs index 34a9dd7c21..28130b79c9 100644 --- a/compiler/typecheck/TcEnv.hs +++ b/compiler/typecheck/TcEnv.hs @@ -537,11 +537,17 @@ tcExtendLocalTypeEnv lcl_env@(TcLclEnv { tcl_env = lcl_type_env }) tc_ty_things get_tvs (_, ATcId { tct_id = id, tct_info = closed }) tvs = case closed of - ClosedLet -> - ASSERT2( isEmptyVarSet id_tvs, ppr id $$ ppr (idType id) ) tvs - _ -> - tvs `unionVarSet` id_tvs - where id_tvs = tyCoVarsOfType (idType id) + ClosedLet -> ASSERT2( is_closed_type, ppr id $$ ppr (idType id) ) + tvs + _other -> tvs `unionVarSet` id_tvs + where + id_tvs = tyCoVarsOfType (idType id) + is_closed_type = not (anyVarSet isTyVar id_tvs) + -- We only care about being closed wrt /type/ variables + -- E.g. a top-level binding might have a type like + -- foo :: t |> co + -- where co :: * ~ * + -- or some other as-yet-unsolved kind coercion get_tvs (_, ATyVar _ tv) tvs -- See Note [Global TyVars] = tvs `unionVarSet` tyCoVarsOfType (tyVarKind tv) `extendVarSet` tv diff --git a/compiler/typecheck/TcErrors.hs b/compiler/typecheck/TcErrors.hs index 3ba2180826..6710434f29 100644 --- a/compiler/typecheck/TcErrors.hs +++ b/compiler/typecheck/TcErrors.hs @@ -805,9 +805,9 @@ addDeferredBinding ctxt err ct -> addTcEvBind ev_binds_var $ mkWantedEvBind evar err_tm HoleDest hole -> do { -- See Note [Deferred errors for coercion holes] - evar <- newEvVar pred - ; addTcEvBind ev_binds_var $ mkWantedEvBind evar err_tm - ; fillCoercionHole hole (mkTcCoVarCo evar) }} + let co_var = coHoleCoVar hole + ; addTcEvBind ev_binds_var $ mkWantedEvBind co_var err_tm + ; fillCoercionHole hole (mkTcCoVarCo co_var) }} | otherwise -- Do not set any evidence for Given/Derived = return () diff --git a/compiler/typecheck/TcHsSyn.hs b/compiler/typecheck/TcHsSyn.hs index e188466107..8d097f52fb 100644 --- a/compiler/typecheck/TcHsSyn.hs +++ b/compiler/typecheck/TcHsSyn.hs @@ -52,6 +52,7 @@ import TcEvidence import TysPrim import TyCon ( isUnboxedTupleTyCon ) import TysWiredIn +import TyCoRep( CoercionHole(..) ) import Type import Coercion import ConLike @@ -1580,35 +1581,30 @@ zonkTyVarOcc env@(ZonkEnv zonk_unbound_tyvar tv_env _) tv Just tv' -> return (mkTyVarTy tv') zonkCoVarOcc :: ZonkEnv -> CoVar -> TcM Coercion -zonkCoVarOcc env@(ZonkEnv _ tyco_env _) cv +zonkCoVarOcc (ZonkEnv _ tyco_env _) cv | Just cv' <- lookupVarEnv tyco_env cv -- don't look in the knot-tied env = return $ mkCoVarCo cv' | otherwise - = mkCoVarCo <$> updateVarTypeM (zonkTcTypeToType env) cv - -zonkCoHole :: ZonkEnv -> CoercionHole - -> Role -> Type -> Type -- these are all redundant with - -- the details in the hole, - -- unzonked - -> TcM Coercion -zonkCoHole env h r t1 t2 - = do { contents <- unpackCoercionHole_maybe h + = do { cv' <- zonkCoVar cv; return (mkCoVarCo cv') } + +zonkCoHole :: ZonkEnv -> CoercionHole -> TcM Coercion +zonkCoHole env hole@(CoercionHole { ch_ref = ref, ch_co_var = cv }) + = do { contents <- readTcRef ref ; case contents of - Just co -> do { co <- zonkCoToCo env co - ; checkCoercionHole co h r t1 t2 } + Just co -> do { co' <- zonkCoToCo env co + ; checkCoercionHole cv co' } -- This next case should happen only in the presence of -- (undeferred) type errors. Originally, I put in a panic -- here, but that caused too many uses of `failIfErrsM`. - Nothing -> do { traceTc "Zonking unfilled coercion hole" (ppr h) + Nothing -> do { traceTc "Zonking unfilled coercion hole" (ppr hole) ; when debugIsOn $ whenNoErrs $ MASSERT2( False , text "Type-correct unfilled coercion hole" - <+> ppr h ) - ; t1 <- zonkTcTypeToType env t1 - ; t2 <- zonkTcTypeToType env t2 - ; return $ mkHoleCo h r t1 t2 } } + <+> ppr hole ) + ; cv' <- zonkCoVar cv + ; return $ mkHoleCo (hole { ch_co_var = cv' }) } } zonk_tycomapper :: TyCoMapper ZonkEnv TcM zonk_tycomapper = TyCoMapper diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs index 0ea08f47bc..bdb11e236c 100644 --- a/compiler/typecheck/TcInteract.hs +++ b/compiler/typecheck/TcInteract.hs @@ -590,7 +590,7 @@ solveOneFromTheOther ev_i ev_w | otherwise = KeepInert - has_binding binds ev = isJust (lookupEvBind binds (ctEvId ev)) + has_binding binds ev = isJust (lookupEvBind binds (ctEvEvId ev)) {- Note [Replacement vs keeping] @@ -990,7 +990,7 @@ interactDict inerts workItem@(CDictCan { cc_ev = ev_w, cc_class = cls, cc_tyargs ; try_inst_res <- shortCutSolver dflags ev_w ev_i ; case try_inst_res of Just evs -> do { flip mapM_ evs $ \ (ev_t, ct_ev, cls, typ) -> - do { setWantedEvBind (ctEvId ct_ev) ev_t + do { setWantedEvBind (ctEvEvId ct_ev) ev_t ; addSolvedDict ct_ev cls typ } ; stopWith ev_w "interactDict/solved from instance" } @@ -2239,7 +2239,7 @@ doTopReactDict inerts work_item@(CDictCan { cc_ev = fl, cc_class = cls finish_wanted theta mk_ev = do { addSolvedDict fl cls xis ; evc_vars <- mapM (newWanted deeper_loc) theta - ; setWantedEvBind (ctEvId fl) (mk_ev (map getEvTerm evc_vars)) + ; setWantedEvBind (ctEvEvId fl) (mk_ev (map getEvTerm evc_vars)) ; emitWorkNC (freshGoals evc_vars) ; stopWith fl "Dict/Top (solved wanted)" } diff --git a/compiler/typecheck/TcMType.hs b/compiler/typecheck/TcMType.hs index 3d451295c4..83a34652d9 100644 --- a/compiler/typecheck/TcMType.hs +++ b/compiler/typecheck/TcMType.hs @@ -79,7 +79,9 @@ module TcMType ( zonkTcType, zonkTcTypes, zonkCo, zonkTyCoVarKind, zonkTcTypeMapper, - zonkEvVar, zonkWC, zonkSimples, zonkId, zonkCt, zonkSkolemInfo, + zonkEvVar, zonkWC, zonkSimples, + zonkId, zonkCoVar, + zonkCt, zonkSkolemInfo, tcGetGlobalTyCoVars, @@ -172,7 +174,7 @@ newWanted :: CtOrigin -> Maybe TypeOrKind -> PredType -> TcM CtEvidence -- Deals with both equality and non-equality predicates newWanted orig t_or_k pty = do loc <- getCtLocM orig t_or_k - d <- if isEqPred pty then HoleDest <$> newCoercionHole + d <- if isEqPred pty then HoleDest <$> newCoercionHole pty else EvVarDest <$> newEvVar pty return $ CtWanted { ctev_dest = d , ctev_pred = pty @@ -210,12 +212,12 @@ emitWanted origin pty -- | Emits a new equality constraint emitWantedEq :: CtOrigin -> TypeOrKind -> Role -> TcType -> TcType -> TcM Coercion emitWantedEq origin t_or_k role ty1 ty2 - = do { hole <- newCoercionHole + = do { hole <- newCoercionHole pty ; loc <- getCtLocM origin (Just t_or_k) ; emitSimple $ mkNonCanonical $ CtWanted { ctev_pred = pty, ctev_dest = HoleDest hole , ctev_nosh = WDeriv, ctev_loc = loc } - ; return (mkHoleCo hole role ty1 ty2) } + ; return (HoleCo hole) } where pty = mkPrimEqPredRole role ty1 ty2 @@ -254,28 +256,28 @@ predTypeOccName ty = case classifyPredType ty of ************************************************************************ -} -newCoercionHole :: TcM CoercionHole -newCoercionHole - = do { u <- newUnique - ; traceTc "New coercion hole:" (ppr u) +newCoercionHole :: TcPredType -> TcM CoercionHole +newCoercionHole pred_ty + = do { co_var <- newEvVar pred_ty + ; traceTc "New coercion hole:" (ppr co_var) ; ref <- newMutVar Nothing - ; return $ CoercionHole u ref } + ; return $ CoercionHole { ch_co_var = co_var, ch_ref = ref } } -- | Put a value in a coercion hole fillCoercionHole :: CoercionHole -> Coercion -> TcM () -fillCoercionHole (CoercionHole u ref) co +fillCoercionHole (CoercionHole { ch_ref = ref, ch_co_var = cv }) co = do { #if defined(DEBUG) ; cts <- readTcRef ref ; whenIsJust cts $ \old_co -> - pprPanic "Filling a filled coercion hole" (ppr u $$ ppr co $$ ppr old_co) + pprPanic "Filling a filled coercion hole" (ppr cv $$ ppr co $$ ppr old_co) #endif - ; traceTc "Filling coercion hole" (ppr u <+> text ":=" <+> ppr co) + ; traceTc "Filling coercion hole" (ppr cv <+> text ":=" <+> ppr co) ; writeTcRef ref (Just co) } -- | Is a coercion hole filled in? isFilledCoercionHole :: CoercionHole -> TcM Bool -isFilledCoercionHole (CoercionHole _ ref) = isJust <$> readTcRef ref +isFilledCoercionHole (CoercionHole { ch_ref = ref }) = isJust <$> readTcRef ref -- | Retrieve the contents of a coercion hole. Panics if the hole -- is unfilled @@ -288,30 +290,36 @@ unpackCoercionHole hole -- | Retrieve the contents of a coercion hole, if it is filled unpackCoercionHole_maybe :: CoercionHole -> TcM (Maybe Coercion) -unpackCoercionHole_maybe (CoercionHole _ ref) = readTcRef ref +unpackCoercionHole_maybe (CoercionHole { ch_ref = ref }) = readTcRef ref -- | Check that a coercion is appropriate for filling a hole. (The hole -- itself is needed only for printing. NB: This must be /lazy/ in the coercion, -- as it's used in TcHsSyn in the presence of knots. -- Always returns the checked coercion, but this return value is necessary -- so that the input coercion is forced only when the output is forced. -checkCoercionHole :: Coercion -> CoercionHole -> Role -> Type -> Type -> TcM Coercion -checkCoercionHole co h r t1 t2 --- co is already zonked, but t1 and t2 might not be +checkCoercionHole :: CoVar -> Coercion -> TcM Coercion +checkCoercionHole cv co | debugIsOn - = do { t1 <- zonkTcType t1 - ; t2 <- zonkTcType t2 - ; let (Pair _t1 _t2, _role) = coercionKindRole co + = do { cv_ty <- zonkTcType (varType cv) + -- co is already zonked, but cv might not be ; return $ - ASSERT2( t1 `eqType` _t1 && t2 `eqType` _t2 && r == _role + ASSERT2( ok cv_ty , (text "Bad coercion hole" <+> - ppr h <> colon <+> vcat [ ppr _t1, ppr _t2, ppr _role - , ppr co, ppr t1, ppr t2 - , ppr r ]) ) + ppr cv <> colon <+> vcat [ ppr t1, ppr t2, ppr role + , ppr cv_ty ]) ) co } | otherwise = return co + where + (Pair t1 t2, role) = coercionKindRole co + ok cv_ty | EqPred cv_rel cv_t1 cv_t2 <- classifyPredType cv_ty + = t1 `eqType` cv_t1 + && t2 `eqType` cv_t2 + && role == eqRelRole cv_rel + | otherwise + = False + {- ************************************************************************ * @@ -1476,6 +1484,9 @@ zonkId id = do { ty' <- zonkTcType (idType id) ; return (Id.setIdType id ty') } +zonkCoVar :: CoVar -> TcM CoVar +zonkCoVar = zonkId + -- | A suitable TyCoMapper for zonking a type inside the knot, and -- before all metavars are filled in. zonkTcTypeMapper :: TyCoMapper () TcM @@ -1486,16 +1497,14 @@ zonkTcTypeMapper = TyCoMapper , tcm_hole = hole , tcm_tybinder = \_env tv _vis -> ((), ) <$> zonkTcTyCoVarBndr tv } where - hole :: () -> CoercionHole -> Role -> Type -> Type - -> TcM Coercion - hole _ h r t1 t2 - = do { contents <- unpackCoercionHole_maybe h + hole :: () -> CoercionHole -> TcM Coercion + hole _ hole@(CoercionHole { ch_ref = ref, ch_co_var = cv }) + = do { contents <- readTcRef ref ; case contents of - Just co -> do { co <- zonkCo co - ; checkCoercionHole co h r t1 t2 } - Nothing -> do { t1 <- zonkTcType t1 - ; t2 <- zonkTcType t2 - ; return $ mkHoleCo h r t1 t2 } } + Just co -> do { co' <- zonkCo co + ; checkCoercionHole cv co' } + Nothing -> do { cv' <- zonkCoVar cv + ; return $ HoleCo (hole { ch_co_var = cv' }) } } -- For unbound, mutable tyvars, zonkType uses the function given to it diff --git a/compiler/typecheck/TcPluginM.hs b/compiler/typecheck/TcPluginM.hs index fe35c4339e..807989e791 100644 --- a/compiler/typecheck/TcPluginM.hs +++ b/compiler/typecheck/TcPluginM.hs @@ -181,8 +181,8 @@ newEvVar :: PredType -> TcPluginM EvVar newEvVar = unsafeTcPluginTcM . TcM.newEvVar -- | Create a fresh coercion hole. -newCoercionHole :: TcPluginM CoercionHole -newCoercionHole = unsafeTcPluginTcM $ TcM.newCoercionHole +newCoercionHole :: PredType -> TcPluginM CoercionHole +newCoercionHole = unsafeTcPluginTcM . TcM.newCoercionHole -- | Bind an evidence variable. This must not be invoked from -- 'tcPluginInit' or 'tcPluginStop', or it will panic. diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs index f9e29a1142..4d7a8e8390 100644 --- a/compiler/typecheck/TcRnTypes.hs +++ b/compiler/typecheck/TcRnTypes.hs @@ -74,11 +74,11 @@ module TcRnTypes( isGivenCt, isHoleCt, isOutOfScopeCt, isExprHoleCt, isTypeHoleCt, isUserTypeErrorCt, getUserTypeErrorMsg, ctEvidence, ctLoc, setCtLoc, ctPred, ctFlavour, ctEqRel, ctOrigin, - mkTcEqPredLikeEv, + ctEvId, mkTcEqPredLikeEv, mkNonCanonical, mkNonCanonicalCt, mkGivens, mkIrredCt, mkInsolubleCt, ctEvPred, ctEvLoc, ctEvOrigin, ctEvEqRel, - ctEvTerm, ctEvCoercion, ctEvId, + ctEvTerm, ctEvCoercion, ctEvEvId, tyCoVarsOfCt, tyCoVarsOfCts, tyCoVarsOfCtList, tyCoVarsOfCtsList, @@ -151,6 +151,7 @@ import TcEvidence import Type import Class ( Class ) import TyCon ( TyCon, tyConKind ) +import TyCoRep ( CoercionHole(..), coHoleCoVar ) import Coercion ( Coercion, mkHoleCo ) import ConLike ( ConLike(..) ) import DataCon ( DataCon, dataConUserType, dataConOrigArgTys ) @@ -1790,6 +1791,10 @@ ctPred :: Ct -> PredType -- See Note [Ct/evidence invariant] ctPred ct = ctEvPred (cc_ev ct) +ctEvId :: Ct -> EvVar +-- The evidence Id for this Ct +ctEvId ct = ctEvEvId (ctEvidence ct) + -- | Makes a new equality predicate with the same role as the given -- evidence. mkTcEqPredLikeEv :: CtEvidence -> TcType -> TcType -> TcType @@ -2644,26 +2649,26 @@ ctEvRole = eqRelRole . ctEvEqRel ctEvTerm :: CtEvidence -> EvTerm ctEvTerm ev@(CtWanted { ctev_dest = HoleDest _ }) = EvCoercion $ ctEvCoercion ev -ctEvTerm ev = EvId (ctEvId ev) +ctEvTerm ev = EvId (ctEvEvId ev) -- Always returns a coercion whose type is precisely ctev_pred of the CtEvidence. -- See also Note [Given in ctEvCoercion] ctEvCoercion :: CtEvidence -> Coercion ctEvCoercion (CtGiven { ctev_pred = pred_ty, ctev_evar = ev_id }) = mkTcCoVarCo (setVarType ev_id pred_ty) -- See Note [Given in ctEvCoercion] -ctEvCoercion (CtWanted { ctev_dest = dest, ctev_pred = pred }) +ctEvCoercion (CtWanted { ctev_dest = dest }) | HoleDest hole <- dest - , Just (role, ty1, ty2) <- getEqPredTys_maybe pred = -- ctEvCoercion is only called on type equalities -- and they always have HoleDests - mkHoleCo hole role ty1 ty2 + mkHoleCo hole ctEvCoercion ev = pprPanic "ctEvCoercion" (ppr ev) -ctEvId :: CtEvidence -> TcId -ctEvId (CtWanted { ctev_dest = EvVarDest ev }) = ev -ctEvId (CtGiven { ctev_evar = ev }) = ev -ctEvId ctev = pprPanic "ctEvId:" (ppr ctev) +ctEvEvId :: CtEvidence -> EvVar +ctEvEvId (CtWanted { ctev_dest = EvVarDest ev }) = ev +ctEvEvId (CtWanted { ctev_dest = HoleDest h }) = coHoleCoVar h +ctEvEvId (CtGiven { ctev_evar = ev }) = ev +ctEvEvId ctev@(CtDerived {}) = pprPanic "ctEvId:" (ppr ctev) instance Outputable TcEvDest where ppr (HoleDest h) = text "hole" <> ppr h diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs index 5755fa1f2e..7926e56d62 100644 --- a/compiler/typecheck/TcSMonad.hs +++ b/compiler/typecheck/TcSMonad.hs @@ -3079,12 +3079,12 @@ emitNewWantedEq loc role ty1 ty2 -- | Make a new equality CtEvidence newWantedEq :: CtLoc -> Role -> TcType -> TcType -> TcS (CtEvidence, Coercion) newWantedEq loc role ty1 ty2 - = do { hole <- wrapTcS $ TcM.newCoercionHole + = do { hole <- wrapTcS $ TcM.newCoercionHole pty ; traceTcS "Emitting new coercion hole" (ppr hole <+> dcolon <+> ppr pty) ; return ( CtWanted { ctev_pred = pty, ctev_dest = HoleDest hole , ctev_nosh = WDeriv , ctev_loc = loc} - , mkHoleCo hole role ty1 ty2 ) } + , mkHoleCo hole ) } where pty = mkPrimEqPredRole role ty1 ty2 diff --git a/compiler/typecheck/TcTyDecls.hs b/compiler/typecheck/TcTyDecls.hs index 87fab6f7fd..548f058811 100644 --- a/compiler/typecheck/TcTyDecls.hs +++ b/compiler/typecheck/TcTyDecls.hs @@ -117,6 +117,7 @@ synonymTyConsOfType ty go_co (ForAllCo _ co co') = go_co co `plusNameEnv` go_co co' go_co (FunCo _ co co') = go_co co `plusNameEnv` go_co co' go_co (CoVarCo _) = emptyNameEnv + go_co (HoleCo {}) = emptyNameEnv go_co (AxiomInstCo _ _ cs) = go_co_s cs go_co (UnivCo p _ ty ty') = go_prov p `plusNameEnv` go ty `plusNameEnv` go ty' go_co (SymCo co) = go_co co @@ -133,7 +134,6 @@ synonymTyConsOfType ty go_prov (PhantomProv co) = go_co co go_prov (ProofIrrelProv co) = go_co co go_prov (PluginProv _) = emptyNameEnv - go_prov (HoleProv _) = emptyNameEnv go_tc tc | isTypeSynonymTyCon tc = unitNameEnv (tyConName tc) tc | otherwise = emptyNameEnv diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs index 079cc47ff3..441545ce24 100644 --- a/compiler/typecheck/TcType.hs +++ b/compiler/typecheck/TcType.hs @@ -876,7 +876,7 @@ exactTyCoVarsOfType ty = go ty where go ty | Just ty' <- tcView ty = go ty' -- This is the key line - go (TyVarTy tv) = unitVarSet tv `unionVarSet` go (tyVarKind tv) + go (TyVarTy tv) = goVar tv go (TyConApp _ tys) = exactTyCoVarsOfTypes tys go (LitTy {}) = emptyVarSet go (AppTy fun arg) = go fun `unionVarSet` go arg @@ -891,7 +891,8 @@ exactTyCoVarsOfType ty goCo (ForAllCo tv k_co co) = goCo co `delVarSet` tv `unionVarSet` goCo k_co goCo (FunCo _ co1 co2) = goCo co1 `unionVarSet` goCo co2 - goCo (CoVarCo v) = unitVarSet v `unionVarSet` go (varType v) + goCo (CoVarCo v) = goVar v + goCo (HoleCo h) = goVar (coHoleCoVar h) goCo (AxiomInstCo _ _ args) = goCos args goCo (UnivCo p _ t1 t2) = goProv p `unionVarSet` go t1 `unionVarSet` go t2 goCo (SymCo co) = goCo co @@ -910,7 +911,8 @@ exactTyCoVarsOfType ty goProv (PhantomProv kco) = goCo kco goProv (ProofIrrelProv kco) = goCo kco goProv (PluginProv _) = emptyVarSet - goProv (HoleProv _) = emptyVarSet + + goVar v = unitVarSet v `unionVarSet` go (varType v) exactTyCoVarsOfTypes :: [Type] -> TyVarSet exactTyCoVarsOfTypes tys = mapUnionVarSet exactTyCoVarsOfType tys @@ -2340,10 +2342,8 @@ to_tc_mapper | Just var <- lookupVarSet ftvs cv = return $ CoVarCo var | otherwise = CoVarCo <$> updateVarTypeM (to_tc_type ftvs) cv - hole :: VarSet -> CoercionHole -> Role -> Type -> Type - -> Identity Coercion - hole ftvs h r t1 t2 = mkHoleCo h r <$> to_tc_type ftvs t1 - <*> to_tc_type ftvs t2 + hole :: VarSet -> CoercionHole -> Identity Coercion + hole _ hole = pprPanic "toTcType: found a coercion hole" (ppr hole) tybinder :: VarSet -> TyVar -> ArgFlag -> Identity (VarSet, TyVar) tybinder ftvs tv _vis = do { kind' <- to_tc_type ftvs (tyVarKind tv) diff --git a/compiler/typecheck/TcUnify.hs b/compiler/typecheck/TcUnify.hs index ca5396bc57..eb96757f21 100644 --- a/compiler/typecheck/TcUnify.hs +++ b/compiler/typecheck/TcUnify.hs @@ -2056,10 +2056,8 @@ occCheckExpand tv ty go env (TyVarTy tv') | tv == tv' = Nothing | Just tv'' <- lookupVarEnv env tv' = return (mkTyVarTy tv'') - | otherwise = do { k' <- go env (tyVarKind tv') - ; return (mkTyVarTy $ - setTyVarKind tv' k') } - -- See Note [Occurrence checking: look inside kinds] + | otherwise = do { tv'' <- go_var env tv' + ; return (mkTyVarTy tv'') } go _ ty@(LitTy {}) = return ty go env (AppTy ty1 ty2) = do { ty1' <- go env ty1 @@ -2094,6 +2092,12 @@ occCheckExpand tv ty ; return (mkCoercionTy co') } ------------------ + go_var env v = do { k' <- go env (varType v) + ; return (setVarType v k') } + -- Works for TyVar and CoVar + -- See Note [Occurrence checking: look inside kinds] + + ------------------ go_co env (Refl r ty) = do { ty' <- go env ty ; return (mkReflCo r ty') } -- Note: Coercions do not contain type synonyms @@ -2113,8 +2117,10 @@ occCheckExpand tv ty go_co env (FunCo r co1 co2) = do { co1' <- go_co env co1 ; co2' <- go_co env co2 ; return (mkFunCo r co1' co2') } - go_co env (CoVarCo c) = do { k' <- go env (varType c) - ; return (mkCoVarCo (setVarType c k')) } + go_co env (CoVarCo c) = do { c' <- go_var env c + ; return (mkCoVarCo c') } + go_co env (HoleCo h) = do { c' <- go_var env (ch_co_var h) + ; return (HoleCo (h { ch_co_var = c' })) } go_co env (AxiomInstCo ax ind args) = do { args' <- mapM (go_co env) args ; return (mkAxiomInstCo ax ind args') } go_co env (UnivCo p r ty1 ty2) = do { p' <- go_prov env p @@ -2148,7 +2154,6 @@ occCheckExpand tv ty go_prov env (PhantomProv co) = PhantomProv <$> go_co env co go_prov env (ProofIrrelProv co) = ProofIrrelProv <$> go_co env co go_prov _ p@(PluginProv _) = return p - go_prov _ p@(HoleProv _) = return p canUnifyWithPolyType :: DynFlags -> TcTyVarDetails -> Bool canUnifyWithPolyType dflags details diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs index 232265dcb5..8c01460f2e 100644 --- a/compiler/typecheck/TcValidity.hs +++ b/compiler/typecheck/TcValidity.hs @@ -1112,7 +1112,7 @@ dropCasts :: Type -> Type -- See Note [Casts during validity checking] -- This function can turn a well-kinded type into an ill-kinded -- one, so I've kept it local to this module --- To consider: drop only UnivCo(HoleProv) casts +-- To consider: drop only HoleCo casts dropCasts (CastTy ty _) = dropCasts ty dropCasts (AppTy t1 t2) = mkAppTy (dropCasts t1) (dropCasts t2) dropCasts (FunTy t1 t2) = mkFunTy (dropCasts t1) (dropCasts t2) @@ -1971,13 +1971,13 @@ fvCo (CoherenceCo co1 co2) = fvCo co1 ++ fvCo co2 fvCo (KindCo co) = fvCo co fvCo (SubCo co) = fvCo co fvCo (AxiomRuleCo _ cs) = concatMap fvCo cs +fvCo (HoleCo h) = pprPanic "fvCo falls into a hole" (ppr h) fvProv :: UnivCoProvenance -> [TyCoVar] fvProv UnsafeCoerceProv = [] fvProv (PhantomProv co) = fvCo co fvProv (ProofIrrelProv co) = fvCo co fvProv (PluginProv _) = [] -fvProv (HoleProv h) = pprPanic "fvProv falls into a hole" (ppr h) sizeType :: Type -> Int -- Size of a type: the number of variables and constructors diff --git a/compiler/types/Coercion.hs b/compiler/types/Coercion.hs index 99969ee143..2a94755424 100644 --- a/compiler/types/Coercion.hs +++ b/compiler/types/Coercion.hs @@ -772,9 +772,8 @@ mkUnsafeCo role ty1 ty2 = mkUnivCo UnsafeCoerceProv role ty1 ty2 -- | Make a coercion from a coercion hole -mkHoleCo :: CoercionHole -> Role - -> Type -> Type -> Coercion -mkHoleCo h r t1 t2 = mkUnivCo (HoleProv h) r t1 t2 +mkHoleCo :: CoercionHole -> Coercion +mkHoleCo h = HoleCo h -- | Make a universal coercion between two arbitrary types. mkUnivCo :: UnivCoProvenance @@ -1010,7 +1009,6 @@ setNominalRole_maybe (UnivCo prov _ co1 co2) PhantomProv _ -> False -- should always be phantom ProofIrrelProv _ -> True -- it's always safe PluginProv _ -> False -- who knows? This choice is conservative. - HoleProv _ -> False -- no no no. = Just $ UnivCo prov Nominal co1 co2 setNominalRole_maybe _ = Nothing @@ -1102,22 +1100,15 @@ promoteCoercion co = case co of FunCo _ _ _ -> mkNomReflCo liftedTypeKind - CoVarCo {} - -> mkKindCo co - - AxiomInstCo {} - -> mkKindCo co + CoVarCo {} -> mkKindCo co + HoleCo {} -> mkKindCo co + AxiomInstCo {} -> mkKindCo co + AxiomRuleCo {} -> mkKindCo co - UnivCo UnsafeCoerceProv _ t1 t2 - -> mkUnsafeCo Nominal (typeKind t1) (typeKind t2) - UnivCo (PhantomProv kco) _ _ _ - -> kco - UnivCo (ProofIrrelProv kco) _ _ _ - -> kco - UnivCo (PluginProv _) _ _ _ - -> mkKindCo co - UnivCo (HoleProv _) _ _ _ - -> mkKindCo co + UnivCo UnsafeCoerceProv _ t1 t2 -> mkUnsafeCo Nominal (typeKind t1) (typeKind t2) + UnivCo (PhantomProv kco) _ _ _ -> kco + UnivCo (ProofIrrelProv kco) _ _ _ -> kco + UnivCo (PluginProv _) _ _ _ -> mkKindCo co SymCo g -> mkSymCo (promoteCoercion g) @@ -1159,9 +1150,6 @@ promoteCoercion co = case co of SubCo g -> promoteCoercion g - AxiomRuleCo {} - -> mkKindCo co - where Pair ty1 ty2 = coercionKind co ki1 = typeKind ty1 @@ -1660,6 +1648,7 @@ seqCo (ForAllCo tv k co) = seqType (tyVarKind tv) `seq` seqCo k `seq` seqCo co seqCo (FunCo r co1 co2) = r `seq` seqCo co1 `seq` seqCo co2 seqCo (CoVarCo cv) = cv `seq` () +seqCo (HoleCo h) = coHoleCoVar h `seq` () seqCo (AxiomInstCo con ind cos) = con `seq` ind `seq` seqCos cos seqCo (UnivCo p r t1 t2) = seqProv p `seq` r `seq` seqType t1 `seq` seqType t2 @@ -1678,7 +1667,6 @@ seqProv UnsafeCoerceProv = () seqProv (PhantomProv co) = seqCo co seqProv (ProofIrrelProv co) = seqCo co seqProv (PluginProv _) = () -seqProv (HoleProv _) = () seqCos :: [Coercion] -> () seqCos [] = () @@ -1735,6 +1723,7 @@ coercionKind co = go co mkInvForAllTy <$> Pair tv1 tv2 <*> Pair ty1 ty2' go (FunCo _ co1 co2) = mkFunTy <$> go co1 <*> go co2 go (CoVarCo cv) = coVarTypes cv + go (HoleCo h) = coVarTypes (coHoleCoVar h) go (AxiomInstCo ax ind cos) | CoAxBranch { cab_tvs = tvs, cab_cvs = cvs , cab_lhs = lhs, cab_rhs = rhs } <- coAxiomNthBranch ax ind @@ -1816,7 +1805,8 @@ coercionKindRole = go (mkInvForAllTy <$> Pair tv1 tv2 <*> Pair ty1 ty2', r) go (FunCo r co1 co2) = (mkFunTy <$> coercionKind co1 <*> coercionKind co2, r) - go (CoVarCo cv) = (coVarTypes cv, coVarRole cv) + go (CoVarCo cv) = go_var cv + go (HoleCo h) = go_var (coHoleCoVar h) go co@(AxiomInstCo ax _ _) = (coercionKind co, coAxiomRole ax) go (UnivCo _ r ty1 ty2) = (Pair ty1 ty2, r) go (SymCo co) = first swap $ go co @@ -1847,6 +1837,10 @@ coercionKindRole = go go (SubCo co) = (coercionKind co, Representational) go co@(AxiomRuleCo ax _) = (coercionKind co, coaxrRole ax) + ------------- + go_var cv = (coVarTypes cv, coVarRole cv) + + ------------- go_app :: Coercion -> [Coercion] -> (Pair Type, Role) -- Collect up all the arguments and apply all at once -- See Note [Nested InstCos] diff --git a/compiler/types/FamInstEnv.hs b/compiler/types/FamInstEnv.hs index bb0da84ca7..131abda47b 100644 --- a/compiler/types/FamInstEnv.hs +++ b/compiler/types/FamInstEnv.hs @@ -1629,6 +1629,7 @@ allTyVarsInTy = go = unionVarSets [unitVarSet tv, go_co co, go_co h] go_co (FunCo _ c1 c2) = go_co c1 `unionVarSet` go_co c2 go_co (CoVarCo cv) = unitVarSet cv + go_co (HoleCo h) = unitVarSet (coHoleCoVar h) go_co (AxiomInstCo _ _ cos) = go_cos cos go_co (UnivCo p _ t1 t2) = go_prov p `unionVarSet` go t1 `unionVarSet` go t2 go_co (SymCo co) = go_co co @@ -1647,7 +1648,6 @@ allTyVarsInTy = go go_prov (PhantomProv co) = go_co co go_prov (ProofIrrelProv co) = go_co co go_prov (PluginProv _) = emptyVarSet - go_prov (HoleProv _) = emptyVarSet mkFlattenFreshTyName :: Uniquable a => a -> Name mkFlattenFreshTyName unq diff --git a/compiler/types/OptCoercion.hs b/compiler/types/OptCoercion.hs index 1f1b9378dc..e8379ad448 100644 --- a/compiler/types/OptCoercion.hs +++ b/compiler/types/OptCoercion.hs @@ -238,6 +238,8 @@ opt_co4 env sym rep r (CoVarCo cv) cv -- cv1 might have a substituted kind! +opt_co4 _ _ _ _ (HoleCo h) + = pprPanic "opt_univ fell into a hole" (ppr h) opt_co4 env sym rep r (AxiomInstCo con ind cos) -- Do *not* push sym inside top-level axioms @@ -268,7 +270,8 @@ opt_co4 env sym rep r (TransCo co1 co2) in_scope = lcInScopeSet env -opt_co4 env sym rep r co@(NthCo {}) = opt_nth_co env sym rep r co +opt_co4 env sym rep r co@(NthCo {}) + = opt_nth_co env sym rep r co opt_co4 env sym rep r (LRCo lr co) | Just pr_co <- splitAppCo_maybe co @@ -430,8 +433,6 @@ opt_univ env sym prov role oty1 oty2 PhantomProv kco -> PhantomProv $ opt_co4_wrap env sym False Nominal kco ProofIrrelProv kco -> ProofIrrelProv $ opt_co4_wrap env sym False Nominal kco PluginProv _ -> prov - HoleProv h -> pprPanic "opt_univ fell into a hole" (ppr h) - ------------- -- NthCo must be handled separately, because it's the one case where we can't diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs index 55b9e1c8a2..b7d92a2a4e 100644 --- a/compiler/types/TyCoRep.hs +++ b/compiler/types/TyCoRep.hs @@ -31,7 +31,8 @@ module TyCoRep ( -- * Coercions Coercion(..), - UnivCoProvenance(..), CoercionHole(..), + UnivCoProvenance(..), + CoercionHole(..), coHoleCoVar, CoercionN, CoercionR, CoercionP, KindCoercion, -- * Functions over types @@ -846,6 +847,8 @@ data Coercion | SubCo CoercionN -- Turns a ~N into a ~R -- :: N -> R + | HoleCo CoercionHole -- ^ See Note [Coercion holes] + -- Only present during typechecking deriving Data.Data type CoercionN = Coercion -- always nominal @@ -1199,7 +1202,6 @@ data UnivCoProvenance | PluginProv String -- ^ From a plugin, which asserts that this coercion -- is sound. The string is for the use of the plugin. - | HoleProv CoercionHole -- ^ See Note [Coercion holes] deriving Data.Data instance Outputable UnivCoProvenance where @@ -1207,14 +1209,16 @@ instance Outputable UnivCoProvenance where ppr (PhantomProv _) = text "(phantom)" ppr (ProofIrrelProv _) = text "(proof irrel.)" ppr (PluginProv str) = parens (text "plugin" <+> brackets (text str)) - ppr (HoleProv hole) = parens (text "hole" <> ppr hole) -- | A coercion to be filled in by the type-checker. See Note [Coercion holes] data CoercionHole - = CoercionHole { chUnique :: Unique -- ^ used only for debugging - , chCoercion :: IORef (Maybe Coercion) + = CoercionHole { ch_co_var :: CoVar + , ch_ref :: IORef (Maybe Coercion) } +coHoleCoVar :: CoercionHole -> CoVar +coHoleCoVar = ch_co_var + instance Data.Data CoercionHole where -- don't traverse? toConstr _ = abstractConstr "CoercionHole" @@ -1222,7 +1226,7 @@ instance Data.Data CoercionHole where dataTypeOf _ = mkNoRepType "CoercionHole" instance Outputable CoercionHole where - ppr (CoercionHole u _) = braces (ppr u) + ppr (CoercionHole { ch_co_var = cv }) = braces (ppr cv) {- Note [Phantom coercions] @@ -1258,7 +1262,7 @@ For unboxed equalities: - Generate a CoercionHole, a mutable variable just like a unification variable - Wrap the CoercionHole in a Wanted constraint; see TcRnTypes.TcEvDest - - Use the CoercionHole in a Coercion, via HoleProv + - Use the CoercionHole in a Coercion, via HoleCo - Solve the constraint later - When solved, fill in the CoercionHole by side effect, instead of doing the let-binding thing @@ -1277,7 +1281,7 @@ the evidence for unboxed equalities: Other notes about HoleCo: - * INVARIANT: CoercionHole and HoleProv are used only during type checking, + * INVARIANT: CoercionHole and HoleCo are used only during type checking, and should never appear in Core. Just like unification variables; a Type can contain a TcTyVar, but only during type checking. If, one day, we use type-level information to separate out forms that can appear during @@ -1453,7 +1457,9 @@ tyCoFVsOfCo (ForAllCo tv kind_co co) fv_cand in_scope acc tyCoFVsOfCo (FunCo _ co1 co2) fv_cand in_scope acc = (tyCoFVsOfCo co1 `unionFV` tyCoFVsOfCo co2) fv_cand in_scope acc tyCoFVsOfCo (CoVarCo v) fv_cand in_scope acc - = (unitFV v `unionFV` tyCoFVsOfType (varType v)) fv_cand in_scope acc + = tyCoFVsOfCoVar v fv_cand in_scope acc +tyCoFVsOfCo (HoleCo h) fv_cand in_scope acc + = tyCoFVsOfCoVar (coHoleCoVar h) fv_cand in_scope acc tyCoFVsOfCo (AxiomInstCo _ _ cos) fv_cand in_scope acc = tyCoFVsOfCos cos fv_cand in_scope acc tyCoFVsOfCo (UnivCo p _ t1 t2) fv_cand in_scope acc = (tyCoFVsOfProv p `unionFV` tyCoFVsOfType t1 @@ -1468,6 +1474,10 @@ tyCoFVsOfCo (KindCo co) fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in tyCoFVsOfCo (SubCo co) fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc tyCoFVsOfCo (AxiomRuleCo _ cs) fv_cand in_scope acc = tyCoFVsOfCos cs fv_cand in_scope acc +tyCoFVsOfCoVar :: CoVar -> FV +tyCoFVsOfCoVar v fv_cand in_scope acc + = (unitFV v `unionFV` tyCoFVsOfType (varType v)) fv_cand in_scope acc + tyCoVarsOfProv :: UnivCoProvenance -> TyCoVarSet tyCoVarsOfProv prov = fvVarSet $ tyCoFVsOfProv prov @@ -1476,7 +1486,6 @@ tyCoFVsOfProv UnsafeCoerceProv fv_cand in_scope acc = emptyFV fv_cand in_scop tyCoFVsOfProv (PhantomProv co) fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc tyCoFVsOfProv (ProofIrrelProv co) fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc tyCoFVsOfProv (PluginProv _) fv_cand in_scope acc = emptyFV fv_cand in_scope acc -tyCoFVsOfProv (HoleProv _) fv_cand in_scope acc = emptyFV fv_cand in_scope acc tyCoVarsOfCos :: [Coercion] -> TyCoVarSet tyCoVarsOfCos cos = fvVarSet $ tyCoFVsOfCos cos @@ -1512,26 +1521,29 @@ coVarsOfCo (TyConAppCo _ _ args) = coVarsOfCos args coVarsOfCo (AppCo co arg) = coVarsOfCo co `unionVarSet` coVarsOfCo arg coVarsOfCo (ForAllCo tv kind_co co) = coVarsOfCo co `delVarSet` tv `unionVarSet` coVarsOfCo kind_co -coVarsOfCo (FunCo _ co1 co2) = coVarsOfCo co1 `unionVarSet` coVarsOfCo co2 -coVarsOfCo (CoVarCo v) = unitVarSet v `unionVarSet` coVarsOfType (varType v) -coVarsOfCo (AxiomInstCo _ _ args) = coVarsOfCos args -coVarsOfCo (UnivCo p _ t1 t2) = coVarsOfProv p `unionVarSet` coVarsOfTypes [t1, t2] -coVarsOfCo (SymCo co) = coVarsOfCo co -coVarsOfCo (TransCo co1 co2) = coVarsOfCo co1 `unionVarSet` coVarsOfCo co2 -coVarsOfCo (NthCo _ co) = coVarsOfCo co -coVarsOfCo (LRCo _ co) = coVarsOfCo co -coVarsOfCo (InstCo co arg) = coVarsOfCo co `unionVarSet` coVarsOfCo arg -coVarsOfCo (CoherenceCo c1 c2) = coVarsOfCos [c1, c2] -coVarsOfCo (KindCo co) = coVarsOfCo co -coVarsOfCo (SubCo co) = coVarsOfCo co -coVarsOfCo (AxiomRuleCo _ cs) = coVarsOfCos cs +coVarsOfCo (FunCo _ co1 co2) = coVarsOfCo co1 `unionVarSet` coVarsOfCo co2 +coVarsOfCo (CoVarCo v) = coVarsOfCoVar v +coVarsOfCo (HoleCo h) = coVarsOfCoVar (coHoleCoVar h) +coVarsOfCo (AxiomInstCo _ _ as) = coVarsOfCos as +coVarsOfCo (UnivCo p _ t1 t2) = coVarsOfProv p `unionVarSet` coVarsOfTypes [t1, t2] +coVarsOfCo (SymCo co) = coVarsOfCo co +coVarsOfCo (TransCo co1 co2) = coVarsOfCo co1 `unionVarSet` coVarsOfCo co2 +coVarsOfCo (NthCo _ co) = coVarsOfCo co +coVarsOfCo (LRCo _ co) = coVarsOfCo co +coVarsOfCo (InstCo co arg) = coVarsOfCo co `unionVarSet` coVarsOfCo arg +coVarsOfCo (CoherenceCo c1 c2) = coVarsOfCos [c1, c2] +coVarsOfCo (KindCo co) = coVarsOfCo co +coVarsOfCo (SubCo co) = coVarsOfCo co +coVarsOfCo (AxiomRuleCo _ cs) = coVarsOfCos cs + +coVarsOfCoVar :: CoVar -> CoVarSet +coVarsOfCoVar v = unitVarSet v `unionVarSet` coVarsOfType (varType v) coVarsOfProv :: UnivCoProvenance -> CoVarSet coVarsOfProv UnsafeCoerceProv = emptyVarSet coVarsOfProv (PhantomProv co) = coVarsOfCo co coVarsOfProv (ProofIrrelProv co) = coVarsOfCo co coVarsOfProv (PluginProv _) = emptyVarSet -coVarsOfProv (HoleProv _) = emptyVarSet coVarsOfCos :: [Coercion] -> CoVarSet coVarsOfCos cos = mapUnionVarSet coVarsOfCo cos @@ -1616,6 +1628,7 @@ noFreeVarsOfCo (AppCo c1 c2) = noFreeVarsOfCo c1 && noFreeVarsOfCo c2 noFreeVarsOfCo co@(ForAllCo {}) = isEmptyVarSet (tyCoVarsOfCo co) noFreeVarsOfCo (FunCo _ c1 c2) = noFreeVarsOfCo c1 && noFreeVarsOfCo c2 noFreeVarsOfCo (CoVarCo _) = False +noFreeVarsOfCo (HoleCo {}) = True -- I'm unsure; probably never happens noFreeVarsOfCo (AxiomInstCo _ _ args) = all noFreeVarsOfCo args noFreeVarsOfCo (UnivCo p _ t1 t2) = noFreeVarsOfProv p && noFreeVarsOfType t1 && @@ -1637,7 +1650,6 @@ noFreeVarsOfProv UnsafeCoerceProv = True noFreeVarsOfProv (PhantomProv co) = noFreeVarsOfCo co noFreeVarsOfProv (ProofIrrelProv co) = noFreeVarsOfCo co noFreeVarsOfProv (PluginProv {}) = True -noFreeVarsOfProv (HoleProv {}) = True -- matches with coVarsOfProv, but I'm unsure {- %************************************************************************ @@ -2123,7 +2135,7 @@ isValidTCvSubst (TCvSubst in_scope tenv cenv) = -- Note [The substitution invariant]. checkValidSubst :: HasCallStack => TCvSubst -> [Type] -> [Coercion] -> a -> a checkValidSubst subst@(TCvSubst in_scope tenv cenv) tys cos a - = ASSERT2( isValidTCvSubst subst, + = WARN( not (isValidTCvSubst subst), text "in_scope" <+> ppr in_scope $$ text "tenv" <+> ppr tenv $$ text "tenvFVs" @@ -2133,7 +2145,7 @@ checkValidSubst subst@(TCvSubst in_scope tenv cenv) tys cos a <+> ppr (tyCoVarsOfCosSet cenv) $$ text "tys" <+> ppr tys $$ text "cos" <+> ppr cos ) - ASSERT2( tysCosFVsInScope, + WARN( not tysCosFVsInScope, text "in_scope" <+> ppr in_scope $$ text "tenv" <+> ppr tenv $$ text "cenv" <+> ppr cenv $$ @@ -2299,16 +2311,18 @@ subst_co subst co go (SubCo co) = mkSubCo $! (go co) go (AxiomRuleCo c cs) = let cs1 = map go cs in cs1 `seqList` AxiomRuleCo c cs1 + go (HoleCo h) = HoleCo h + -- NB: this last case is a little suspicious, but we need it. Originally, + -- there was a panic here, but it triggered from deeplySkolemise. Because + -- we only skolemise tyvars that are manually bound, this operation makes + -- sense, even over a coercion with holes. We don't need to substitute + -- in the type of the coHoleCoVar because it wouldn't makes sense to have + -- forall a. ....(ty |> {hole_cv::a}).... go_prov UnsafeCoerceProv = UnsafeCoerceProv go_prov (PhantomProv kco) = PhantomProv (go kco) go_prov (ProofIrrelProv kco) = ProofIrrelProv (go kco) go_prov p@(PluginProv _) = p - go_prov p@(HoleProv _) = p - -- NB: this last case is a little suspicious, but we need it. Originally, - -- there was a panic here, but it triggered from deeplySkolemise. Because - -- we only skolemise tyvars that are manually bound, this operation makes - -- sense, even over a coercion with holes. substForAllCoBndr :: TCvSubst -> TyVar -> Coercion -> (TCvSubst, TyVar, Coercion) substForAllCoBndr subst @@ -2335,7 +2349,7 @@ substForAllCoBndrCallback sym sco (TCvSubst in_scope tenv cenv) where new_env | no_change && not sym = delVarEnv tenv old_var | sym = extendVarEnv tenv old_var $ - TyVarTy new_var `CastTy` new_kind_co + TyVarTy new_var `CastTy` new_kind_co | otherwise = extendVarEnv tenv old_var (TyVarTy new_var) no_kind_change = noFreeVarsOfCo old_kind_co @@ -2882,6 +2896,7 @@ tidyCo env@(_, subst) co go (CoVarCo cv) = case lookupVarEnv subst cv of Nothing -> CoVarCo cv Just cv' -> CoVarCo cv' + go (HoleCo h) = HoleCo h go (AxiomInstCo con ind cos) = let args = map go cos in args `seqList` AxiomInstCo con ind args go (UnivCo p r t1 t2) = (((UnivCo $! (go_prov p)) $! r) $! @@ -2901,7 +2916,6 @@ tidyCo env@(_, subst) co go_prov (PhantomProv co) = PhantomProv (go co) go_prov (ProofIrrelProv co) = ProofIrrelProv (go co) go_prov p@(PluginProv _) = p - go_prov p@(HoleProv _) = p tidyCos :: TidyEnv -> [Coercion] -> [Coercion] tidyCos env = map (tidyCo env) @@ -2943,6 +2957,7 @@ coercionSize (AppCo co arg) = coercionSize co + coercionSize arg coercionSize (ForAllCo _ h co) = 1 + coercionSize co + coercionSize h coercionSize (FunCo _ co1 co2) = 1 + coercionSize co1 + coercionSize co2 coercionSize (CoVarCo _) = 1 +coercionSize (HoleCo _) = 1 coercionSize (AxiomInstCo _ _ args) = 1 + sum (map coercionSize args) coercionSize (UnivCo p _ t1 t2) = 1 + provSize p + typeSize t1 + typeSize t2 coercionSize (SymCo co) = 1 + coercionSize co @@ -2960,4 +2975,3 @@ provSize UnsafeCoerceProv = 1 provSize (PhantomProv co) = 1 + coercionSize co provSize (ProofIrrelProv co) = 1 + coercionSize co provSize (PluginProv _) = 1 -provSize (HoleProv h) = pprPanic "provSize hits a hole" (ppr h) diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs index 3b4983477c..817627076a 100644 --- a/compiler/types/Type.hs +++ b/compiler/types/Type.hs @@ -435,13 +435,15 @@ expandTypeSynonyms ty = mkKindCo (go_co subst co) go_co subst (SubCo co) = mkSubCo (go_co subst co) - go_co subst (AxiomRuleCo ax cs) = AxiomRuleCo ax (map (go_co subst) cs) + go_co subst (AxiomRuleCo ax cs) + = AxiomRuleCo ax (map (go_co subst) cs) + go_co _ (HoleCo h) + = pprPanic "expandTypeSynonyms hit a hole" (ppr h) go_prov _ UnsafeCoerceProv = UnsafeCoerceProv go_prov subst (PhantomProv co) = PhantomProv (go_co subst co) go_prov subst (ProofIrrelProv co) = ProofIrrelProv (go_co subst co) go_prov _ p@(PluginProv _) = p - go_prov _ (HoleProv h) = pprPanic "expandTypeSynonyms hit a hole" (ppr h) -- the "False" and "const" are to accommodate the type of -- substForAllCoBndrCallback, which is general enough to @@ -496,10 +498,9 @@ data TyCoMapper env m -- constructors? , tcm_tyvar :: env -> TyVar -> m Type , tcm_covar :: env -> CoVar -> m Coercion - , tcm_hole :: env -> CoercionHole -> Role - -> Type -> Type -> m Coercion - -- ^ What to do with coercion holes. See Note [Coercion holes] in - -- TyCoRep. + , tcm_hole :: env -> CoercionHole -> m Coercion + -- ^ What to do with coercion holes. + -- See Note [Coercion holes] in TyCoRep. , tcm_tybinder :: env -> TyVar -> ArgFlag -> m (env, TyVar) -- ^ The returned env is used in the extended scope @@ -552,8 +553,7 @@ mapCoercion mapper@(TyCoMapper { tcm_smart = smart, tcm_covar = covar go (CoVarCo cv) = covar env cv go (AxiomInstCo ax i args) = mkaxiominstco ax i <$> mapM go args - go (UnivCo (HoleProv hole) r t1 t2) - = cohole env hole r t1 t2 + go (HoleCo hole) = cohole env hole go (UnivCo p r t1 t2) = mkunivco <$> go_prov p <*> pure r <*> mapType mapper env t1 <*> mapType mapper env t2 @@ -571,7 +571,6 @@ mapCoercion mapper@(TyCoMapper { tcm_smart = smart, tcm_covar = covar go_prov (PhantomProv co) = PhantomProv <$> go co go_prov (ProofIrrelProv co) = ProofIrrelProv <$> go co go_prov p@(PluginProv _) = return p - go_prov (HoleProv _) = panic "mapCoercion" ( mktyconappco, mkappco, mkaxiominstco, mkunivco , mksymco, mktransco, mknthco, mklrco, mkinstco, mkcoherenceco @@ -2366,6 +2365,7 @@ tyConsOfType ty go_co (AxiomInstCo ax _ args) = go_ax ax `unionUniqSets` go_cos args go_co (UnivCo p _ t1 t2) = go_prov p `unionUniqSets` go t1 `unionUniqSets` go t2 go_co (CoVarCo {}) = emptyUniqSet + go_co (HoleCo {}) = emptyUniqSet go_co (SymCo co) = go_co co go_co (TransCo co1 co2) = go_co co1 `unionUniqSets` go_co co2 go_co (NthCo _ co) = go_co co @@ -2380,7 +2380,6 @@ tyConsOfType ty go_prov (PhantomProv co) = go_co co go_prov (ProofIrrelProv co) = go_co co go_prov (PluginProv _) = emptyUniqSet - go_prov (HoleProv _) = emptyUniqSet -- this last case can happen from the tyConsOfType used from -- checkTauTvUpdate |