[Git][ghc/ghc][wip/cfuneqcan-refactor] Do mightMatchLater correctlier.
Richard Eisenberg
gitlab at gitlab.haskell.org
Wed Nov 4 20:48:57 UTC 2020
Richard Eisenberg pushed to branch wip/cfuneqcan-refactor at Glasgow Haskell Compiler / GHC
Commits:
5a9c4936 by Richard Eisenberg at 2020-11-04T15:48:36-05:00
Do mightMatchLater correctlier.
- - - - -
3 changed files:
- compiler/GHC/Core/Type.hs
- compiler/GHC/Core/Unify.hs
- compiler/GHC/Tc/Solver/Monad.hs
Changes:
=====================================
compiler/GHC/Core/Type.hs
=====================================
@@ -156,7 +156,7 @@ module GHC.Core.Type (
coVarsOfType,
coVarsOfTypes,
- anyFreeVarsOfType,
+ anyFreeVarsOfType, anyFreeVarsOfTypes,
noFreeVarsOfType,
splitVisVarsOfType, splitVisVarsOfTypes,
expandTypeSynonyms,
=====================================
compiler/GHC/Core/Unify.hs
=====================================
@@ -1790,9 +1790,9 @@ flattenTys is defined here because of module dependencies.
-}
data FlattenEnv
- = FlattenEnv { fe_type_map :: TypeMap TyVar
+ = FlattenEnv { fe_type_map :: TypeMap (TyVar, TyCon, [Type])
-- domain: exactly-saturated type family applications
- -- range: fresh variables
+ -- range: (fresh variable, type family tycon, args)
, fe_in_scope :: InScopeSet }
-- See Note [Flattening]
@@ -1808,15 +1808,26 @@ flattenTys :: InScopeSet -> [Type] -> [Type]
-- See Note [Flattening]
flattenTys in_scope tys = fst (flattenTysX in_scope tys)
-flattenTysX :: InScopeSet -> [Type] -> ([Type], TyVarSet)
+flattenTysX :: InScopeSet -> [Type] -> ([Type], TyVarEnv (TyCon, [Type]))
-- See Note [Flattening]
-- NB: the returned types mention the fresh type variables
--- in the returned set. We don't return the
--- mapping from those fresh vars to the ty-fam
--- applications they stand for (we could, but no need)
+-- in the domain of the returned env, whose range includes
+-- the original type family applications. Building a substitution
+-- from this information and applying it would yield the original
+-- types -- almost. The problem is that the original type might
+-- have something like (forall b. F a b); the returned environment
+-- can't really sensibly refer to that b. So it may include a locally-
+-- bound tyvar in its range. Currently, the only usage of this env't
+-- checks whether there are any meta-variables in it
+-- (in GHC.Tc.Solver.Monad.mightMatchLater), so this is all OK.
flattenTysX in_scope tys
= let (env, result) = coreFlattenTys emptyTvSubstEnv (emptyFlattenEnv in_scope) tys in
- (result, foldTM (flip extendVarSet) (fe_type_map env) emptyVarSet)
+ (result, build_env (fe_type_map env))
+ where
+ build_env :: TypeMap (TyVar, TyCon, [Type]) -> TyVarEnv (TyCon, [Type])
+ build_env env_in
+ = foldTM (\(tv, tc, tys) env_out -> extendVarEnv env_out tv (tc, tys))
+ env_in emptyVarEnv
coreFlattenTys :: TvSubstEnv -> FlattenEnv
-> [Type] -> (FlattenEnv, [Type])
@@ -1899,15 +1910,17 @@ coreFlattenTyFamApp :: TvSubstEnv -> FlattenEnv
-> (FlattenEnv, Type)
coreFlattenTyFamApp tv_subst env fam_tc fam_args
= case lookupTypeMap type_map fam_ty of
- Just tv -> (env', mkAppTys (mkTyVarTy tv) leftover_args')
- Nothing -> let tyvar_name = mkFlattenFreshTyName fam_tc
- tv = uniqAway in_scope $
- mkTyVar tyvar_name (typeKind fam_ty)
-
- ty' = mkAppTys (mkTyVarTy tv) leftover_args'
- env'' = env' { fe_type_map = extendTypeMap type_map fam_ty tv
- , fe_in_scope = extendInScopeSet in_scope tv }
- in (env'', ty')
+ Just (tv, _, _) -> (env', mkAppTys (mkTyVarTy tv) leftover_args')
+ Nothing ->
+ let tyvar_name = mkFlattenFreshTyName fam_tc
+ tv = uniqAway in_scope $
+ mkTyVar tyvar_name (typeKind fam_ty)
+
+ ty' = mkAppTys (mkTyVarTy tv) leftover_args'
+ env'' = env' { fe_type_map = extendTypeMap type_map fam_ty
+ (tv, fam_tc, sat_fam_args)
+ , fe_in_scope = extendInScopeSet in_scope tv }
+ in (env'', ty')
where
arity = tyConArity fam_tc
tcv_subst = TCvSubst (fe_in_scope env) tv_subst emptyVarEnv
=====================================
compiler/GHC/Tc/Solver/Monad.hs
=====================================
@@ -1,6 +1,6 @@
{-# LANGUAGE CPP, DeriveFunctor, TypeFamilies, ScopedTypeVariables #-}
-{-# OPTIONS_GHC -Wno-incomplete-record-updates #-}
+{-# OPTIONS_GHC -Wno-incomplete-record-updates -Wno-incomplete-uni-patterns #-}
-- | Type definitions for the constraint solver
module GHC.Tc.Solver.Monad (
@@ -2129,25 +2129,20 @@ mightMatchLater given_pred given_loc wanted_pred wanted_loc
| prohibitedSuperClassSolve given_loc wanted_loc
= False
- | SurelyApart <- tcUnifyTysFG bind_meta_tv flattened_given flattened_wanted
+ | SurelyApart <- tcUnifyTysFG bind_meta_tv [flattened_given] [flattened_wanted]
= False
| otherwise
= True -- safe answer
where
- given_in_scope = mkInScopeSet $ tyCoVarsOfType given_pred
- wanted_in_scope = mkInScopeSet $ tyCoVarsOfType wanted_pred
+ in_scope = mkInScopeSet $ tyCoVarsOfTypes [given_pred, wanted_pred]
- (flattened_given, given_vars)
- | anyFreeVarsOfType isMetaTyVar given_pred
- = flattenTysX given_in_scope [given_pred]
- | otherwise
- = ([given_pred], emptyVarSet)
-
- (flattened_wanted, wanted_vars)
- = flattenTysX wanted_in_scope [wanted_pred]
-
- all_flat_vars = given_vars `unionVarSet` wanted_vars
+ -- NB: flatten both at the same time, so that we can share mappings
+ -- from type family applications to variables, and also to guarantee
+ -- that the fresh variables are really fresh between the given and
+ -- the wanted.
+ ([flattened_given, flattened_wanted], var_mapping)
+ = flattenTysX in_scope [given_pred, wanted_pred]
bind_meta_tv :: TcTyVar -> BindFlag
-- Any meta tyvar may be unified later, so we treat it as
@@ -2156,12 +2151,17 @@ mightMatchLater given_pred given_loc wanted_pred wanted_loc
-- something that matches the 'given', until demonstrated
-- otherwise. More info in Note [Instance and Given overlap]
-- in GHC.Tc.Solver.Interact
- bind_meta_tv tv | isMetaTyVar tv
- , not (isCycleBreakerTyVar tv) = BindMe
- -- a cycle-breaker var really stands for a type family
- -- application where all variables are skolems
- | tv `elemVarSet` all_flat_vars = BindMe
- | otherwise = Skolem
+ bind_meta_tv tv | is_meta_tv tv = BindMe
+
+ | Just (_fam_tc, fam_args) <- lookupVarEnv var_mapping tv
+ , anyFreeVarsOfTypes is_meta_tv fam_args
+ = BindMe
+
+ | otherwise = Skolem
+
+ -- CycleBreakerTvs really stands for a type family application in
+ -- a given; these won't contain touchable meta-variables
+ is_meta_tv = isMetaTyVar <&&> not . isCycleBreakerTyVar
prohibitedSuperClassSolve :: CtLoc -> CtLoc -> Bool
-- See Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance
@@ -2187,30 +2187,21 @@ in the Wanted might be arbitrarily instantiated. We do *not* want
to allow skolems in the Given to be instantiated. But what about
type family applications?
-We break this down into two cases: a type family application in the
-Given, and a type family application in the Wanted.
-
-* Given: Before ever looking at Wanteds, we process and simplify all
-the Givens. So any type family applications in a Given have already
-been fully reduced. Furthermore, future Wanteds won't rewrite Givens,
-so information we learn later can't come to bear. So we worry about
-reduction of a type family application in a Given only when it has
-an metavariable in it (necessarily unfilled, because these types
-have been zonked before getting here). A Given with a metavariable
-is rare, but it can happen. See typecheck/should_compile/InstanceGivenOverlap2,
-which uses partial type signatures and polykinds to pull it off.
-
-* Wanted: Unlike the Given case, a type family application in a
-Wanted is always a cause for concern. Further information might allow
-it to reduce, so we want to say that a type family application could
-unify with any type.
-
-How we do this: we use the *core* flattener, as defined in the
-flattenTys function. See Note [Flattening] in GHC.Core.Unify. This
-function takes any type family application and turns it into a fresh
-variable. These fresh variables must be flagged with BindMe in the
-bind_meta_tv function, so that the unifier will match them. This
-is the only reason we need to collect them here.
+To allow flexibility in how type family applications unify we use
+the Core flattener. See Note [Flattening] in GHC.Core.Unify.
+This is *distinct* from the flattener in GHC.Tc.Solver.Flatten.
+The Core flattener replaces all type family applications with
+fresh variables. The next question: should we allow these fresh
+variables in the domian of a unifying substitution?
+
+A type family application that mentions only skolems is settled: any
+skolems would have been rewritten w.r.t. Givens by now. These type
+family applications match only themselves. A type family application
+that mentions metavariables, on the other hand, can match anything.
+So, if the original type family application contains a metavariable,
+we use BindMe to tell the unifier to allow it in the substitution.
+On the other hand, a type family application with only skolems is
+considered rigid.
Note [When does an implication have given equalities?]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/5a9c493677d0ccbab27eaa467a0b095dbd6daef1
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/5a9c493677d0ccbab27eaa467a0b095dbd6daef1
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/20201104/367c5228/attachment-0001.html>
More information about the ghc-commits
mailing list