[Git][ghc/ghc][wip/cfuneqcan-refactor] Subtleties in Note [Instance and Given overlap]
Richard Eisenberg
gitlab at gitlab.haskell.org
Mon Nov 2 23:02:41 UTC 2020
Richard Eisenberg pushed to branch wip/cfuneqcan-refactor at Glasgow Haskell Compiler / GHC
Commits:
ebfebd6f by Richard Eisenberg at 2020-11-02T18:02:22-05:00
Subtleties in Note [Instance and Given overlap]
- - - - -
7 changed files:
- compiler/GHC/Core/Map/Type.hs
- compiler/GHC/Core/TyCo/FVs.hs
- compiler/GHC/Core/Type.hs
- compiler/GHC/Core/Unify.hs
- compiler/GHC/Tc/Solver/Interact.hs
- compiler/GHC/Tc/Solver/Monad.hs
- testsuite/tests/typecheck/should_compile/all.T
Changes:
=====================================
compiler/GHC/Core/Map/Type.hs
=====================================
@@ -8,6 +8,9 @@
{-# LANGUAGE TypeFamilies #-}
module GHC.Core.Map.Type (
+ -- * Re-export generic interface
+ TrieMap(..),
+
-- * Maps over 'Type's
TypeMap, emptyTypeMap, extendTypeMap, lookupTypeMap, foldTypeMap,
LooseTypeMap,
=====================================
compiler/GHC/Core/TyCo/FVs.hs
=====================================
@@ -26,7 +26,8 @@ module GHC.Core.TyCo.FVs
injectiveVarsOfType, injectiveVarsOfTypes,
invisibleVarsOfType, invisibleVarsOfTypes,
- -- No Free vars
+ -- Any and No Free vars
+ anyFreeVarsOfType, anyFreeVarsOfTypes, anyFreeVarsOfCo,
noFreeVarsOfType, noFreeVarsOfTypes, noFreeVarsOfCo,
-- * Well-scoped free variables
@@ -47,7 +48,7 @@ import GHC.Prelude
import {-# SOURCE #-} GHC.Core.Type (coreView, partitionInvisibleTypes)
-import Data.Monoid as DM ( Endo(..), All(..) )
+import Data.Monoid as DM ( Endo(..), Any(..) )
import GHC.Core.TyCo.Rep
import GHC.Core.TyCon
import GHC.Types.Var
@@ -855,32 +856,43 @@ invisibleVarsOfTypes = mapUnionFV invisibleVarsOfType
{- *********************************************************************
* *
- No free vars
+ Any free vars
* *
********************************************************************* -}
-nfvFolder :: TyCoFolder TyCoVarSet DM.All
-nfvFolder = TyCoFolder { tcf_view = noView
- , tcf_tyvar = do_tcv, tcf_covar = do_tcv
- , tcf_hole = do_hole, tcf_tycobinder = do_bndr }
+{-# INLINE afvFolder #-} -- so that specialization to (const True) works
+afvFolder :: (TyCoVar -> Bool) -> TyCoFolder TyCoVarSet DM.Any
+afvFolder check_fv = TyCoFolder { tcf_view = noView
+ , tcf_tyvar = do_tcv, tcf_covar = do_tcv
+ , tcf_hole = do_hole, tcf_tycobinder = do_bndr }
where
- do_tcv is tv = All (tv `elemVarSet` is)
- do_hole _ _ = All True -- I'm unsure; probably never happens
+ do_tcv is tv = Any (not (tv `elemVarSet` is) && check_fv tv)
+ do_hole _ _ = Any False -- I'm unsure; probably never happens
do_bndr is tv _ = is `extendVarSet` tv
-nfv_ty :: Type -> DM.All
-nfv_tys :: [Type] -> DM.All
-nfv_co :: Coercion -> DM.All
-(nfv_ty, nfv_tys, nfv_co, _) = foldTyCo nfvFolder emptyVarSet
+anyFreeVarsOfType :: (TyCoVar -> Bool) -> Type -> Bool
+anyFreeVarsOfType check_fv ty = DM.getAny (f ty)
+ where (f, _, _, _) = foldTyCo (afvFolder check_fv) emptyVarSet
+
+anyFreeVarsOfTypes :: (TyCoVar -> Bool) -> [Type] -> Bool
+anyFreeVarsOfTypes check_fv tys = DM.getAny (f tys)
+ where (_, f, _, _) = foldTyCo (afvFolder check_fv) emptyVarSet
+
+anyFreeVarsOfCo :: (TyCoVar -> Bool) -> Coercion -> Bool
+anyFreeVarsOfCo check_fv co = DM.getAny (f co)
+ where (_, _, f, _) = foldTyCo (afvFolder check_fv) emptyVarSet
noFreeVarsOfType :: Type -> Bool
-noFreeVarsOfType ty = DM.getAll (nfv_ty ty)
+noFreeVarsOfType ty = not $ DM.getAny (f ty)
+ where (f, _, _, _) = foldTyCo (afvFolder (const True)) emptyVarSet
noFreeVarsOfTypes :: [Type] -> Bool
-noFreeVarsOfTypes tys = DM.getAll (nfv_tys tys)
+noFreeVarsOfTypes tys = not $ DM.getAny (f tys)
+ where (_, f, _, _) = foldTyCo (afvFolder (const True)) emptyVarSet
noFreeVarsOfCo :: Coercion -> Bool
-noFreeVarsOfCo co = getAll (nfv_co co)
+noFreeVarsOfCo co = not $ DM.getAny (f co)
+ where (_, _, f, _) = foldTyCo (afvFolder (const True)) emptyVarSet
{- *********************************************************************
@@ -983,4 +995,3 @@ tyCoVarsOfTypeWellScoped = scopedSort . tyCoVarsOfTypeList
-- | Get the free vars of types in scoped order
tyCoVarsOfTypesWellScoped :: [Type] -> [TyVar]
tyCoVarsOfTypesWellScoped = scopedSort . tyCoVarsOfTypesList
-
=====================================
compiler/GHC/Core/Type.hs
=====================================
@@ -156,6 +156,7 @@ module GHC.Core.Type (
coVarsOfType,
coVarsOfTypes,
+ anyFreeVarsOfType,
noFreeVarsOfType,
splitVisVarsOfType, splitVisVarsOfTypes,
expandTypeSynonyms,
=====================================
compiler/GHC/Core/Unify.hs
=====================================
@@ -24,7 +24,7 @@ module GHC.Core.Unify (
liftCoMatch,
-- The core flattening algorithm
- flattenTys
+ flattenTys, flattenTysX
) where
#include "HsVersions.h"
@@ -1806,12 +1806,17 @@ updateInScopeSet env upd = env { fe_in_scope = upd (fe_in_scope env) }
flattenTys :: InScopeSet -> [Type] -> [Type]
-- See Note [Flattening]
--- NB: the returned types may mention fresh type variables,
--- arising from the flattening. We don't return the
+flattenTys in_scope tys = fst (flattenTysX in_scope tys)
+
+flattenTysX :: InScopeSet -> [Type] -> ([Type], TyVarSet)
+-- 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)
-flattenTys in_scope tys
- = snd $ coreFlattenTys emptyTvSubstEnv (emptyFlattenEnv in_scope) tys
+flattenTysX in_scope tys
+ = let (env, result) = coreFlattenTys emptyTvSubstEnv (emptyFlattenEnv in_scope) tys in
+ (result, foldTM (flip extendVarSet) (fe_type_map env) emptyVarSet)
coreFlattenTys :: TvSubstEnv -> FlattenEnv
-> [Type] -> (FlattenEnv, [Type])
=====================================
compiler/GHC/Tc/Solver/Interact.hs
=====================================
@@ -2116,12 +2116,7 @@ Other notes:
- natural numbers
- Typeable
-* Flatten-skolems: we do not treat a flatten-skolem as unifiable
- for this purpose.
- E.g. f :: Eq (F a) => [a] -> [a]
- f xs = ....(xs==xs).....
- Here we get [W] Eq [a], and we don't want to refrain from solving
- it because of the given (Eq (F a)) constraint!
+* See also Note [What might match later?] in GHC.Tc.Solver.Monad.
* The given-overlap problem is arguably not easy to appear in practice
due to our aggressive prioritization of equality solving over other
=====================================
compiler/GHC/Tc/Solver/Monad.hs
=====================================
@@ -2124,10 +2124,31 @@ matchableGivens loc_w pred_w (IS { inert_cans = inert_cans })
= False
mightMatchLater :: TcPredType -> CtLoc -> TcPredType -> CtLoc -> Bool
+-- See Note [What might match later?]
mightMatchLater given_pred given_loc wanted_pred wanted_loc
- = not (prohibitedSuperClassSolve given_loc wanted_loc)
- && isJust (tcUnifyTys bind_meta_tv [given_pred] [wanted_pred])
+ | prohibitedSuperClassSolve given_loc wanted_loc
+ = False
+
+ | 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
+
+ (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
+
bind_meta_tv :: TcTyVar -> BindFlag
-- Any meta tyvar may be unified later, so we treat it as
-- bindable when unifying with givens. That ensures that we
@@ -2135,8 +2156,12 @@ 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 = BindMe
- | otherwise = Skolem
+ 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
prohibitedSuperClassSolve :: CtLoc -> CtLoc -> Bool
-- See Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance
@@ -2154,6 +2179,39 @@ because it is a candidate for floating out of this implication. We
only float equalities with a meta-tyvar on the left, so we only pull
those out here.
+Note [What might match later?]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We must determine whether a Given might later match a Wanted. We
+definitely need to account for the possibility that any metavariable
+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.
+
Note [When does an implication have given equalities?]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider an implication
=====================================
testsuite/tests/typecheck/should_compile/all.T
=====================================
@@ -723,3 +723,6 @@ test('T18470', normal, compile, [''])
test('T18323', normal, compile, [''])
test('T18585', normal, compile, [''])
test('T15942', normal, compile, [''])
+test('CbvOverlap', normal, compile, [''])
+test('InstanceGivenOverlap', normal, compile, [''])
+test('InstanceGivenOverlap2', normal, compile, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/ebfebd6fd6e6407bc0c8ad81d31616b76fc8ce3d
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/ebfebd6fd6e6407bc0c8ad81d31616b76fc8ce3d
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/20201102/1bb0e635/attachment-0001.html>
More information about the ghc-commits
mailing list