[Git][ghc/ghc][wip/T19044] Fix #19044 by tweaking unification in inst lookup
Richard Eisenberg
gitlab at gitlab.haskell.org
Fri Dec 11 19:23:00 UTC 2020
Richard Eisenberg pushed to branch wip/T19044 at Glasgow Haskell Compiler / GHC
Commits:
9ea5ac77 by Richard Eisenberg at 2020-12-11T14:22:38-05:00
Fix #19044 by tweaking unification in inst lookup
See Note [Infinitary substitution in lookup] in GHC.Core.InstEnv
Test case: typecheck/should_compile/T19044
Close #19044
- - - - -
4 changed files:
- compiler/GHC/Core/InstEnv.hs
- compiler/GHC/Core/Unify.hs
- + testsuite/tests/typecheck/should_compile/T19044.hs
- testsuite/tests/typecheck/should_compile/all.T
Changes:
=====================================
compiler/GHC/Core/InstEnv.hs
=====================================
@@ -760,6 +760,47 @@ When we match this against D [ty], we return the instantiating types
where the 'Nothing' indicates that 'b' can be freely instantiated.
(The caller instantiates it to a flexi type variable, which will
presumably later become fixed via functional dependencies.)
+
+Note [Infinitary substitution in lookup]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+
+ class C a b
+ instance C c c
+ instance C d (Maybe d)
+ [W] C e (Maybe e)
+
+You would think we could just use the second instance, because the first doesn't
+unify. But that's just ever so slightly wrong. The reason we check for unifiers
+along with matchers is that we don't want the possibility that a type variable
+instantiation could cause an instance choice to change. Yet if we have
+ type family M = Maybe M
+and choose (e |-> M), then both instances match. This is absurd, but we cannot
+rule it out. Yet, worrying about this case is awfully inconvenient to users,
+and so we pretend the problem doesn't exist, by considering a lookup runs into
+this occurs-check issue to indicate that an instance surely does not apply (i.e.
+is like the SurelyApart case).
+
+Why don't we just exclude any instances that are MaybeApart? Because we might
+have a [W] C e (F e), where F is a type family. The second instance above does
+not match, but it should be included as a future possibility. Unification will
+return MaybeApart MARTypeFamily in this case.
+
+What can go wrong with this design choice? We might get incoherence -- but not
+loss of type safety. In particular, if we have [W] C M M (for the M type family
+above), then GHC might arbitrarily choose either instance, depending on how
+M reduces (or doesn't).
+
+For type families, we can't just ignore the problem (as we essentially do here),
+because doing so would give us a hole in the type safety proof (as explored in
+Section 6 of "Closed Type Families with Overlapping Equations", POPL'14). This
+possibility of an infinitary substitution manifests as closed type families that
+look like they should reduce, but don't. Users complain: #9082 and #17311. For
+open type families, we actually can have unsoundness if we don't take infinitary
+substitutions into account: #8162. But, luckily, for class instances, we just
+risk coherence -- not great, but it seems better to give users what they likely
+want. (Also, note that this problem existed for the entire decade of 201x without
+anyone noticing, so it's manifestly not ruining anyone's day.)
-}
-- |Look up an instance in the given instance environment. The given class application must match exactly
@@ -839,8 +880,10 @@ lookupInstEnv' ie vis_mods cls tys
-- We consider MaybeApart to be a case where the instance might
-- apply in the future. This covers an instance like C Int and
-- a target like [W] C (F a), where F is a type family.
- SurelyApart -> find ms us rest
- _ -> find ms (item:us) rest
+ SurelyApart -> find ms us rest
+ -- Note [Infinitary substitution in lookup]
+ MaybeApart MARInfinite _ -> find ms us rest
+ _ -> find ms (item:us) rest
where
tpl_tv_set = mkVarSet tpl_tvs
tys_tv_set = tyCoVarsOfTypes tys
=====================================
compiler/GHC/Core/Unify.hs
=====================================
@@ -18,7 +18,7 @@ module GHC.Core.Unify (
tcUnifyTy, tcUnifyTyKi, tcUnifyTys, tcUnifyTyKis,
tcUnifyTysFG, tcUnifyTyWithTFs,
BindFlag(..),
- UnifyResult, UnifyResultM(..),
+ UnifyResult, UnifyResultM(..), MaybeApartReason(..),
-- Matching a type against a lifted type (coercion)
liftCoMatch,
@@ -391,8 +391,8 @@ tcUnifyTyWithTFs twoWay t1 t2
= case tc_unify_tys (const BindMe) twoWay True False
rn_env emptyTvSubstEnv emptyCvSubstEnv
[t1] [t2] of
- Unifiable (subst, _) -> Just $ maybe_fix subst
- MaybeApart (subst, _) -> Just $ maybe_fix subst
+ Unifiable (subst, _) -> Just $ maybe_fix subst
+ MaybeApart _reason (subst, _) -> Just $ maybe_fix subst
-- we want to *succeed* in questionable cases. This is a
-- pre-unification algorithm.
SurelyApart -> Nothing
@@ -432,12 +432,23 @@ tcUnifyTyKis bind_fn tys1 tys2
-- return the final result. See Note [Fine-grained unification]
type UnifyResult = UnifyResultM TCvSubst
data UnifyResultM a = Unifiable a -- the subst that unifies the types
- | MaybeApart a -- the subst has as much as we know
+ | MaybeApart MaybeApartReason
+ a -- the subst has as much as we know
-- it must be part of a most general unifier
-- See Note [The substitution in MaybeApart]
| SurelyApart
deriving Functor
+-- | Why are two types 'MaybeApart'? 'MARTypeFamily' takes precedence.
+-- This is used (only) in Note [Infinitary substitution in lookup] in GHC.Core.InstEnv
+data MaybeApartReason = MARInfinite -- ^ matching e.g. a ~? Maybe a
+ | MARTypeFamily -- ^ matching e.g. F Int ~? Bool
+ deriving (Eq, Ord)
+
+instance Outputable MaybeApartReason where
+ ppr MARInfinite = text "MARInfinite"
+ ppr MARTypeFamily = text "MARTypeFamily"
+
instance Applicative UnifyResultM where
pure = Unifiable
(<*>) = ap
@@ -445,9 +456,10 @@ instance Applicative UnifyResultM where
instance Monad UnifyResultM where
SurelyApart >>= _ = SurelyApart
- MaybeApart x >>= f = case f x of
- Unifiable y -> MaybeApart y
- other -> other
+ MaybeApart r1 x >>= f = case f x of
+ Unifiable y -> MaybeApart r1 y
+ MaybeApart r2 y -> MaybeApart (max r1 r2) y
+ SurelyApart -> SurelyApart
Unifiable x >>= f = f x
instance Alternative UnifyResultM where
@@ -530,9 +542,9 @@ tc_unify_tys bind_fn unif inj_check match_kis rn_env tv_env cv_env tys1 tys2
kis2 = map typeKind tys2
instance Outputable a => Outputable (UnifyResultM a) where
- ppr SurelyApart = text "SurelyApart"
- ppr (Unifiable x) = text "Unifiable" <+> ppr x
- ppr (MaybeApart x) = text "MaybeApart" <+> ppr x
+ ppr SurelyApart = text "SurelyApart"
+ ppr (Unifiable x) = text "Unifiable" <+> ppr x
+ ppr (MaybeApart r x) = text "MaybeApart" <+> ppr r <+> ppr x
{-
************************************************************************
@@ -994,7 +1006,7 @@ unify_ty env ty1 ty2 _kco
; unify_tys env inj_tys1 inj_tys2
; unless (um_inj_tf env) $ -- See (end of) Note [Specification of unification]
- don'tBeSoSure $ unify_tys env noninj_tys1 noninj_tys2 }
+ don'tBeSoSure MARTypeFamily $ unify_tys env noninj_tys1 noninj_tys2 }
| Just (tc1, _) <- mb_tc_app1
, not (isGenerativeTyCon tc1 Nominal)
@@ -1002,7 +1014,7 @@ unify_ty env ty1 ty2 _kco
-- because the (F ty1) behaves like a variable
-- NB: if unifying, we have already dealt
-- with the 'ty2 = variable' case
- = maybeApart
+ = maybeApart MARTypeFamily
| Just (tc2, _) <- mb_tc_app2
, not (isGenerativeTyCon tc2 Nominal)
@@ -1010,7 +1022,7 @@ unify_ty env ty1 ty2 _kco
-- E.g. unify_ty [a] (F ty2) = MaybeApart, when unifying (only)
-- because the (F ty2) behaves like a variable
-- NB: we have already dealt with the 'ty1 = variable' case
- = maybeApart
+ = maybeApart MARTypeFamily
where
mb_tc_app1 = tcSplitTyConApp_maybe ty1
@@ -1190,7 +1202,7 @@ bindTv env tv1 ty2
-- Make sure you include 'kco' (which ty2 does) #14846
; occurs <- occursCheck env tv1 free_tvs2
- ; if occurs then maybeApart
+ ; if occurs then maybeApart MARInfinite
else extendTvEnv tv1 ty2 }
occursCheck :: UMEnv -> TyVar -> VarSet -> UM Bool
@@ -1291,9 +1303,9 @@ initUM :: TvSubstEnv -- subst to extend
-> UM a -> UnifyResultM a
initUM subst_env cv_subst_env um
= case unUM um state of
- Unifiable (_, subst) -> Unifiable subst
- MaybeApart (_, subst) -> MaybeApart subst
- SurelyApart -> SurelyApart
+ Unifiable (_, subst) -> Unifiable subst
+ MaybeApart r (_, subst) -> MaybeApart r subst
+ SurelyApart -> SurelyApart
where
state = UMState { um_tv_env = subst_env
, um_cv_env = cv_subst_env }
@@ -1333,9 +1345,7 @@ checkRnEnv :: UMEnv -> VarSet -> UM ()
checkRnEnv env varset
| isEmptyVarSet skol_vars = return ()
| varset `disjointVarSet` skol_vars = return ()
- | otherwise = maybeApart
- -- ToDo: why MaybeApart?
- -- I think SurelyApart would be right
+ | otherwise = surelyApart
where
skol_vars = um_skols env
-- NB: That isEmptyVarSet guard is a critical optimization;
@@ -1343,10 +1353,10 @@ checkRnEnv env varset
-- the type, often saving quite a bit of allocation.
-- | Converts any SurelyApart to a MaybeApart
-don'tBeSoSure :: UM () -> UM ()
-don'tBeSoSure um = UM $ \ state ->
+don'tBeSoSure :: MaybeApartReason -> UM () -> UM ()
+don'tBeSoSure r um = UM $ \ state ->
case unUM um state of
- SurelyApart -> MaybeApart (state, ())
+ SurelyApart -> MaybeApart r (state, ())
other -> other
umRnOccL :: UMEnv -> TyVar -> TyVar
@@ -1358,8 +1368,8 @@ umRnOccR env v = rnOccR (um_rn_env env) v
umSwapRn :: UMEnv -> UMEnv
umSwapRn env = env { um_rn_env = rnSwap (um_rn_env env) }
-maybeApart :: UM ()
-maybeApart = UM (\state -> MaybeApart (state, ()))
+maybeApart :: MaybeApartReason -> UM ()
+maybeApart r = UM (\state -> MaybeApart r (state, ()))
surelyApart :: UM a
surelyApart = UM (\_ -> SurelyApart)
=====================================
testsuite/tests/typecheck/should_compile/T19044.hs
=====================================
@@ -0,0 +1,20 @@
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+module T19044 where
+
+class C a b where
+ m :: a -> b
+
+instance C a a where
+ m = id
+
+instance C a (Maybe a) where
+ m _ = Nothing
+
+f :: a -> Maybe a
+f = g
+ where
+ g x = h (m x) x
+
+h :: Maybe a -> a -> Maybe a
+h = const
=====================================
testsuite/tests/typecheck/should_compile/all.T
=====================================
@@ -734,6 +734,7 @@ test('T17186', normal, compile, [''])
test('CbvOverlap', normal, compile, [''])
test('InstanceGivenOverlap', normal, compile, [''])
test('InstanceGivenOverlap2', normal, compile, [''])
+test('T19044', normal, compile, [''])
test('LocalGivenEqs', normal, compile, [''])
test('LocalGivenEqs2', normal, compile, [''])
test('T18891', normal, compile, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/9ea5ac7742d2f1baa5d68f3a578561f2d106fc84
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/9ea5ac7742d2f1baa5d68f3a578561f2d106fc84
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/20201211/44a01069/attachment-0001.html>
More information about the ghc-commits
mailing list