Commit 9766b0c8 authored by Richard Eisenberg's avatar Richard Eisenberg
Browse files

Fix #12442.

The problem is described in the ticket.

This patch adds new variants of the access points to the pure
unifier that allow unification of types only when the caller
wants this behavior. (The unifier used to also unify kinds.)
This behavior is appropriate when the kinds are either already
known to be the same, or the list of types provided are a
list of well-typed arguments to some type constructor. In the
latter case, unifying earlier types in the list will unify the
kinds of any later (dependent) types.

At use sites, I went through and chose the unification function
according to the criteria above.

This patch includes some modest performance improvements as we
are now doing less work.
parent 3a17916b
......@@ -945,7 +945,7 @@ findPtrTyss i tys = foldM step (i, []) tys
-- The types can contain skolem type variables, which need to be treated as normal vars.
-- In particular, we want them to unify with things.
improveRTTIType :: HscEnv -> RttiType -> RttiType -> Maybe TCvSubst
improveRTTIType _ base_ty new_ty = U.tcUnifyTy base_ty new_ty
improveRTTIType _ base_ty new_ty = U.tcUnifyTyKi base_ty new_ty
getDataConArgTys :: DataCon -> Type -> TR [Type]
-- Given the result type ty of a constructor application (D a b c :: ty)
......
......@@ -51,7 +51,7 @@ import Name ( Name, NamedThing(..), nameIsLocalOrFrom )
import NameSet
import NameEnv
import UniqFM
import Unify ( ruleMatchTyX )
import Unify ( ruleMatchTyKiX )
import BasicTypes ( Activation, CompilerPhase, isActive, pprRuleName )
import StaticFlags ( opt_PprStyle_Debug )
import DynFlags ( DynFlags )
......@@ -947,7 +947,7 @@ match_ty :: RuleMatchEnv
match_ty renv subst ty1 ty2
= do { tv_subst'
<- Unify.ruleMatchTyX (rv_tmpls renv) (rv_lcl renv) tv_subst ty1 ty2
<- Unify.ruleMatchTyKiX (rv_tmpls renv) (rv_lcl renv) tv_subst ty1 ty2
; return (subst { rs_tv_subst = tv_subst' }) }
where
tv_subst = rs_tv_subst subst
......
......@@ -257,9 +257,9 @@ improveClsFD clas_tvs fd
length tys_inst == length clas_tvs
, ppr tys_inst <+> ppr tys_actual )
case tcMatchTys ltys1 ltys2 of
case tcMatchTyKis ltys1 ltys2 of
Nothing -> []
Just subst | isJust (tcMatchTysX subst rtys1 rtys2)
Just subst | isJust (tcMatchTyKisX subst rtys1 rtys2)
-- Don't include any equations that already hold.
-- Reason: then we know if any actual improvement has happened,
-- in which case we need to iterate the solver
......@@ -592,12 +592,12 @@ checkFunDeps inst_envs (ClsInst { is_tvs = qtvs1, is_cls = cls
| instanceCantMatch trimmed_tcs rough_tcs2
= False
| otherwise
= case tcUnifyTys bind_fn ltys1 ltys2 of
= case tcUnifyTyKis bind_fn ltys1 ltys2 of
Nothing -> False
Just subst
-> isNothing $ -- Bogus legacy test (Trac #10675)
-- See Note [Bogus consistency check]
tcUnifyTys bind_fn (substTysUnchecked subst rtys1) (substTysUnchecked subst rtys2)
tcUnifyTyKis bind_fn (substTysUnchecked subst rtys1) (substTysUnchecked subst rtys2)
where
trimmed_tcs = trimRoughMatchTcs cls_tvs fd rough_tcs1
......
......@@ -38,7 +38,7 @@ import TcType
import TrieMap () -- DV: for now
import Type
import TysWiredIn ( ptrRepLiftedTy )
import Unify ( tcMatchTy )
import Unify ( tcMatchTyKi )
import Util
import Var
import VarSet
......@@ -2075,8 +2075,8 @@ disambigGroup (default_ty:default_tys) group@(the_tv, wanteds)
= return False
the_ty = mkTyVarTy the_tv
mb_subst = tcMatchTy the_ty default_ty
-- Make sure the kinds match too; hence this call to tcMatchTy
mb_subst = tcMatchTyKi the_ty default_ty
-- Make sure the kinds match too; hence this call to tcMatchTyKi
-- E.g. suppose the only constraint was (Typeable k (a::k))
-- With the addition of polykinded defaulting we also want to reject
-- ill-kinded defaulting attempts like (Eq []) or (Foldable Int) here.
......
......@@ -5,16 +5,18 @@
{-# LANGUAGE DeriveFunctor #-}
module Unify (
tcMatchTy, tcMatchTys, tcMatchTyX, tcMatchTysX, tcUnifyTyWithTFs,
ruleMatchTyX,
tcMatchTy, tcMatchTyKi,
tcMatchTys, tcMatchTyKis,
tcMatchTyX, tcMatchTysX, tcMatchTyKisX,
ruleMatchTyKiX,
-- * Rough matching
roughMatchTcs, instanceCantMatch,
typesCantMatch,
-- Side-effect free unification
tcUnifyTy, tcUnifyTys,
tcUnifyTysFG,
tcUnifyTy, tcUnifyTyKi, tcUnifyTys, tcUnifyTyKis,
tcUnifyTysFG, tcUnifyTyWithTFs,
BindFlag(..),
UnifyResult, UnifyResultM(..),
......@@ -74,6 +76,8 @@ Unification is much tricker than you might think.
-- The returned substitution might bind coercion variables,
-- if the variable is an argument to a GADT constructor.
--
-- Precondition: typeKind ty1 `eqType` typeKind ty2
--
-- We don't pass in a set of "template variables" to be bound
-- by the match, because tcMatchTy (and similar functions) are
-- always used on top-level types, so we can bind any of the
......@@ -81,6 +85,11 @@ Unification is much tricker than you might think.
tcMatchTy :: Type -> Type -> Maybe TCvSubst
tcMatchTy ty1 ty2 = tcMatchTys [ty1] [ty2]
-- | Like 'tcMatchTy', but allows the kinds of the types to differ,
-- and thus matches them as well.
tcMatchTyKi :: Type -> Type -> Maybe TCvSubst
tcMatchTyKi ty1 ty2 = tcMatchTyKis [ty1] [ty2]
-- | This is similar to 'tcMatchTy', but extends a substitution
tcMatchTyX :: TCvSubst -- ^ Substitution to extend
-> Type -- ^ Template
......@@ -98,16 +107,42 @@ tcMatchTys tys1 tys2
where
in_scope = mkInScopeSet (tyCoVarsOfTypes tys1 `unionVarSet` tyCoVarsOfTypes tys2)
-- | Like 'tcMatchTyKi' but over a list of types.
tcMatchTyKis :: [Type] -- ^ Template
-> [Type] -- ^ Target
-> Maybe TCvSubst -- ^ One-shot substitution
tcMatchTyKis tys1 tys2
= tcMatchTyKisX (mkEmptyTCvSubst in_scope) tys1 tys2
where
in_scope = mkInScopeSet (tyCoVarsOfTypes tys1 `unionVarSet` tyCoVarsOfTypes tys2)
-- | Like 'tcMatchTys', but extending a substitution
tcMatchTysX :: TCvSubst -- ^ Substitution to extend
-> [Type] -- ^ Template
-> [Type] -- ^ Target
-> Maybe TCvSubst -- ^ One-shot substitution
tcMatchTysX (TCvSubst in_scope tv_env cv_env) tys1 tys2
-- See Note [Kind coercions in Unify]
tcMatchTysX subst tys1 tys2
= tc_match_tys_x False subst tys1 tys2
-- | Like 'tcMatchTyKis', but extending a substitution
tcMatchTyKisX :: TCvSubst -- ^ Substitution to extend
-> [Type] -- ^ Template
-> [Type] -- ^ Target
-> Maybe TCvSubst -- ^ One-shot subtitution
tcMatchTyKisX subst tys1 tys2
= tc_match_tys_x True subst tys1 tys2
-- | Worker for 'tcMatchTysX' and 'tcMatchTyKisX'
tc_match_tys_x :: Bool -- ^ match kinds?
-> TCvSubst
-> [Type]
-> [Type]
-> Maybe TCvSubst
tc_match_tys_x match_kis (TCvSubst in_scope tv_env cv_env) tys1 tys2
= case tc_unify_tys (const BindMe)
False -- Matching, not unifying
False -- Not an injectivity check
match_kis
(mkRnEnv2 in_scope) tv_env cv_env tys1 tys2 of
Unifiable (tv_env', cv_env')
-> Just $ TCvSubst in_scope tv_env' cv_env'
......@@ -115,17 +150,18 @@ tcMatchTysX (TCvSubst in_scope tv_env cv_env) tys1 tys2
-- | This one is called from the expression matcher,
-- which already has a MatchEnv in hand
ruleMatchTyX
ruleMatchTyKiX
:: TyCoVarSet -- ^ template variables
-> RnEnv2
-> TvSubstEnv -- ^ type substitution to extend
-> Type -- ^ Template
-> Type -- ^ Target
-> Maybe TvSubstEnv
ruleMatchTyX tmpl_tvs rn_env tenv tmpl target
ruleMatchTyKiX tmpl_tvs rn_env tenv tmpl target
-- See Note [Kind coercions in Unify]
= case tc_unify_tys (matchBindFun tmpl_tvs) False False rn_env
tenv emptyCvSubstEnv [tmpl] [target] of
= case tc_unify_tys (matchBindFun tmpl_tvs) False False
True -- <-- this means to match the kinds
rn_env tenv emptyCvSubstEnv [tmpl] [target] of
Unifiable (tenv', _) -> Just tenv'
_ -> Nothing
......@@ -294,14 +330,20 @@ which can't tell the difference between MaybeApart and SurelyApart, so those
usages won't notice this design choice.
-}
-- | Simple unification of two types; all type variables are bindable
-- Precondition: the kinds are already equal
tcUnifyTy :: Type -> Type -- All tyvars are bindable
-> Maybe TCvSubst
-- A regular one-shot (idempotent) substitution
-- Simple unification of two types; all type variables are bindable
tcUnifyTy t1 t2 = tcUnifyTys (const BindMe) [t1] [t2]
-- | Like 'tcUnifyTy', but also unifies the kinds
tcUnifyTyKi :: Type -> Type -> Maybe TCvSubst
tcUnifyTyKi t1 t2 = tcUnifyTyKis (const BindMe) [t1] [t2]
-- | Unify two types, treating type family applications as possibly unifying
-- with anything and looking through injective type family applications.
-- Precondition: kinds are the same
tcUnifyTyWithTFs :: Bool -- ^ True <=> do two-way unification;
-- False <=> do one-way matching.
-- See end of sec 5.2 from the paper
......@@ -311,7 +353,7 @@ tcUnifyTyWithTFs :: Bool -- ^ True <=> do two-way unification;
-- The code is incorporated with the standard unifier for convenience, but
-- its operation should match the specification in the paper.
tcUnifyTyWithTFs twoWay t1 t2
= case tc_unify_tys (const BindMe) twoWay True
= case tc_unify_tys (const BindMe) twoWay True False
rn_env emptyTvSubstEnv emptyCvSubstEnv
[t1] [t2] of
Unifiable (subst, _) -> Just $ niFixTCvSubst subst
......@@ -337,6 +379,15 @@ tcUnifyTys bind_fn tys1 tys2
Unifiable result -> Just result
_ -> Nothing
-- | Like 'tcUnifyTys' but also unifies the kinds
tcUnifyTyKis :: (TyCoVar -> BindFlag)
-> [Type] -> [Type]
-> Maybe TCvSubst
tcUnifyTyKis bind_fn tys1 tys2
= case tcUnifyTyKisFG bind_fn tys1 tys2 of
Unifiable result -> Just result
_ -> Nothing
-- This type does double-duty. It is used in the UM (unifier monad) and to
-- return the final result. See Note [Fine-grained unification]
type UnifyResult = UnifyResultM TCvSubst
......@@ -373,12 +424,26 @@ instance MonadPlus UnifyResultM
-- | @tcUnifyTysFG bind_tv tys1 tys2@ attepts to find a substitution @s@ (whose
-- domain elements all respond 'BindMe' to @bind_tv@) such that
-- @s(tys1)@ and that of @s(tys2)@ are equal, as witnessed by the returned
-- Coercions.
-- Coercions. This version requires that the kinds of the types are the same,
-- if you unify left-to-right.
tcUnifyTysFG :: (TyVar -> BindFlag)
-> [Type] -> [Type]
-> UnifyResult
tcUnifyTysFG bind_fn tys1 tys2
= do { (env, _) <- tc_unify_tys bind_fn True False env
= tc_unify_tys_fg False bind_fn tys1 tys2
tcUnifyTyKisFG :: (TyVar -> BindFlag)
-> [Type] -> [Type]
-> UnifyResult
tcUnifyTyKisFG bind_fn tys1 tys2
= tc_unify_tys_fg True bind_fn tys1 tys2
tc_unify_tys_fg :: Bool
-> (TyVar -> BindFlag)
-> [Type] -> [Type]
-> UnifyResult
tc_unify_tys_fg match_kis bind_fn tys1 tys2
= do { (env, _) <- tc_unify_tys bind_fn True False match_kis env
emptyTvSubstEnv emptyCvSubstEnv
tys1 tys2
; return $ niFixTCvSubst env }
......@@ -391,14 +456,16 @@ tcUnifyTysFG bind_fn tys1 tys2
tc_unify_tys :: (TyVar -> BindFlag)
-> Bool -- ^ True <=> unify; False <=> match
-> Bool -- ^ True <=> doing an injectivity check
-> Bool -- ^ True <=> treat the kinds as well
-> RnEnv2
-> TvSubstEnv -- ^ substitution to extend
-> CvSubstEnv
-> [Type] -> [Type]
-> UnifyResultM (TvSubstEnv, CvSubstEnv)
tc_unify_tys bind_fn unif inj_check rn_env tv_env cv_env tys1 tys2
tc_unify_tys bind_fn unif inj_check match_kis rn_env tv_env cv_env tys1 tys2
= initUM bind_fn unif inj_check rn_env tv_env cv_env $
do { unify_tys kis1 kis2
do { when match_kis $
unify_tys kis1 kis2
; unify_tys tys1 tys2
; (,) <$> getTvSubstEnv <*> getCvSubstEnv }
where
......@@ -684,8 +751,16 @@ For AppTy, we must unify the kinds of the functions, but once these are
unified, we can continue unifying arguments without worrying further about
kinds.
The interface to this module includes both "...Ty" functions and
"...TyKi" functions. The former assume that INVARIANT is already
established, either because the kinds are the same or because the
list of types being passed in are the well-typed arguments to some
type constructor (see two paragraphs above). The latter take a separate
pre-pass over the kinds to establish INVARIANT. Sometimes, it's important
not to take the second pass, as it caused #12442.
We thought, at one point, that this was all unnecessary: why should
casts be in types in the first place? But they do. In
casts be in types in the first place? But they are sometimes. In
dependent/should_compile/KindEqualities2, we see, for example the
constraint Num (Int |> (blah ; sym blah)). We naturally want to find
a dictionary for that constraint, which requires dealing with
......
-- Based on https://github.com/idris-lang/Idris-dev/blob/v0.9.10/libs/effects/Effects.idr
{-# LANGUAGE TypeInType, ScopedTypeVariables, TypeOperators, TypeApplications,
GADTs, TypeFamilies, AllowAmbiguousTypes #-}
module T12442 where
import Data.Kind
data family Sing (a :: k)
data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>
type family (a :: k1 ~> k2) @@ (b :: k1) :: k2
data TyCon1 :: (Type -> Type) -> (Type ~> Type)
type instance (TyCon1 t) @@ x = t x
data TyCon2 :: (Type -> Type -> Type) -> (Type ~> Type ~> Type)
type instance (TyCon2 t) @@ x = (TyCon1 (t x))
data TyCon3 :: (Type -> Type -> Type -> Type) -> (Type ~> Type ~> Type ~> Type)
type instance (TyCon3 t) @@ x = (TyCon2 (t x))
type Effect = Type ~> Type ~> Type ~> Type
data EFFECT :: Type where
MkEff :: Type -> Effect -> EFFECT
data EffElem :: (Type ~> Type ~> Type ~> Type) -> Type -> [EFFECT] -> Type where
Here :: EffElem x a (MkEff a x ': xs)
data instance Sing (elem :: EffElem x a xs) where
SHere :: Sing Here
type family UpdateResTy b t (xs :: [EFFECT]) (elem :: EffElem e a xs)
(thing :: e @@ a @@ b @@ t) :: [EFFECT] where
UpdateResTy b _ (MkEff a e ': xs) Here n = MkEff b e ': xs
data EffM :: (Type ~> Type) -> [EFFECT] -> [EFFECT] -> Type -> Type
effect :: forall e a b t xs prf eff m.
Sing (prf :: EffElem e a xs)
-> Sing (eff :: e @@ a @@ b @@ t)
-> EffM m xs (UpdateResTy b t xs prf eff) t
effect = undefined
data State :: Type -> Type -> Type -> Type where
Get :: State a a a
data instance Sing (e :: State a b c) where
SGet :: Sing Get
type STATE t = MkEff t (TyCon3 State)
get_ :: forall m x. EffM m '[STATE x] '[STATE x] x
get_ = effect @(TyCon3 State) SHere SGet
......@@ -21,3 +21,4 @@ test('T11711', normal, compile, [''])
test('RaeJobTalk', normal, compile, [''])
test('T11635', normal, compile, [''])
test('T11719', normal, compile, [''])
test('T12442', normal, compile, [''])
......@@ -585,7 +585,7 @@ test('T5837',
# 2014-12-08: 115905208 Constraint solver perf improvements (esp kick-out)
# 2016-04-06: 24199320 (x86/Linux, 64-bit machine) TypeInType
(wordsize(64), 48507272, 10)])
(wordsize(64), 42445672, 10)])
# sample: 3926235424 (amd64/Linux, 15/2/2012)
# 2012-10-02 81879216
# 2012-09-20 87254264 amd64/Linux
......@@ -604,6 +604,7 @@ test('T5837',
# 2015-12-11 43877520 amd64/Linux, TypeInType (see #11196)
# 2016-03-18 48507272 Mac, accept small regression in exchange
# for other optimisations
# 2016-09-15 42445672 Linux; fixing #12422
],
compile_fail,['-freduction-depth=50'])
......@@ -715,13 +716,14 @@ test('T9872a',
test('T9872b',
[ only_ways(['normal']),
compiler_stats_num_field('bytes allocated',
[(wordsize(64), 4600233488, 5),
[(wordsize(64), 4069522928, 5),
# 2014-12-10 6483306280 Initally created
# 2014-12-16 6892251912 Flattener parameterized over roles
# 2014-12-18 3480212048 Reduce type families even more eagerly
# 2015-12-11 5199926080 TypeInType (see #11196)
# 2016-02-08 4918990352 Improved a bit by tyConRolesRepresentational
# 2016-04-06: 4600233488 Refactoring of CSE #11781
# 2016-09-15: 4069522928 Fix #12422
(wordsize(32), 2422750696, 5)
# was 1700000000
# 2016-04-06 2422750696 x86/Linux
......@@ -732,13 +734,14 @@ test('T9872b',
test('T9872c',
[ only_ways(['normal']),
compiler_stats_num_field('bytes allocated',
[(wordsize(64), 4306667256, 5),
[(wordsize(64), 3702580928, 5),
# 2014-12-10 5495850096 Initally created
# 2014-12-16 5842024784 Flattener parameterized over roles
# 2014-12-18 2963554096 Reduce type families even more eagerly
# 2015-12-11 4723613784 TypeInType (see #11196)
# 2016-02-08 4454071184 Improved a bit by tyConRolesRepresentational
# 2016-04-06: 4306667256 Refactoring of CSE #11781
# 2016-09-15: 3702580928 Fixing #12422
(wordsize(32), 2257242896, 5)
# was 1500000000
# 2016-04-06 2257242896
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment