[Git][ghc/ghc][wip/cfuneqcan-refactor] Lots of bug-fixing.
Richard Eisenberg
gitlab at gitlab.haskell.org
Fri Oct 9 20:47:54 UTC 2020
Richard Eisenberg pushed to branch wip/cfuneqcan-refactor at Glasgow Haskell Compiler / GHC
Commits:
c2972870 by Richard Eisenberg at 2020-10-09T16:47:37-04:00
Lots of bug-fixing.
- - - - -
26 changed files:
- compiler/GHC/Core/Coercion.hs
- compiler/GHC/Core/Coercion.hs-boot
- compiler/GHC/Core/Coercion/Opt.hs
- compiler/GHC/Core/FamInstEnv.hs
- compiler/GHC/Core/InstEnv.hs
- compiler/GHC/Core/TyCon.hs
- compiler/GHC/Core/Type.hs
- compiler/GHC/Core/Unify.hs
- compiler/GHC/Tc/Errors.hs
- compiler/GHC/Tc/Solver/Canonical.hs
- compiler/GHC/Tc/Solver/Flatten.hs
- compiler/GHC/Tc/Solver/Monad.hs
- compiler/GHC/Tc/Types/Constraint.hs
- compiler/GHC/Tc/Types/Evidence.hs
- compiler/GHC/Tc/Utils/Unify.hs
- testsuite/tests/indexed-types/should_compile/T3017.stderr
- testsuite/tests/indexed-types/should_fail/T14369.stderr
- testsuite/tests/indexed-types/should_fail/T2544.stderr
- testsuite/tests/indexed-types/should_fail/T2627b.stderr
- testsuite/tests/indexed-types/should_fail/T3330c.stderr
- testsuite/tests/indexed-types/should_fail/T4174.stderr
- testsuite/tests/indexed-types/should_fail/T4179.stderr
- testsuite/tests/indexed-types/should_fail/T4272.stderr
- testsuite/tests/indexed-types/should_fail/T5439.stderr
- testsuite/tests/indexed-types/should_fail/T8227.stderr
- testsuite/tests/indexed-types/should_fail/T8518.stderr
Changes:
=====================================
compiler/GHC/Core/Coercion.hs
=====================================
@@ -1226,7 +1226,7 @@ mkKindCo co
| otherwise
= KindCo co
-mkSubCo :: Coercion -> Coercion
+mkSubCo :: HasDebugCallStack => Coercion -> Coercion
-- Input coercion is Nominal, result is Representational
-- see also Note [Role twiddling functions]
mkSubCo (Refl ty) = GRefl Representational ty MRefl
=====================================
compiler/GHC/Core/Coercion.hs-boot
=====================================
@@ -30,7 +30,7 @@ mkInstCo :: Coercion -> Coercion -> Coercion
mkGReflCo :: Role -> Type -> MCoercionN -> Coercion
mkNomReflCo :: Type -> Coercion
mkKindCo :: Coercion -> Coercion
-mkSubCo :: Coercion -> Coercion
+mkSubCo :: HasDebugCallStack => Coercion -> Coercion
mkProofIrrelCo :: Role -> Coercion -> Coercion -> Coercion -> Coercion
mkAxiomRuleCo :: CoAxiomRule -> [Coercion] -> Coercion
=====================================
compiler/GHC/Core/Coercion/Opt.hs
=====================================
@@ -24,7 +24,6 @@ import GHC.Core.TyCon
import GHC.Core.Coercion.Axiom
import GHC.Types.Var.Set
import GHC.Types.Var.Env
-import GHC.Core.FamInstEnv ( flattenTys )
import GHC.Data.Pair
import GHC.Data.List.SetOps ( getNth )
import GHC.Core.Unify
=====================================
compiler/GHC/Core/FamInstEnv.hs
=====================================
@@ -33,10 +33,7 @@ module GHC.Core.FamInstEnv (
-- Normalisation
topNormaliseType, topNormaliseType_maybe,
normaliseType, normaliseTcApp,
- topReduceTyFamApp_maybe, reduceTyFamApp_maybe,
-
- -- Flattening
- flattenTys
+ topReduceTyFamApp_maybe, reduceTyFamApp_maybe
) where
#include "HsVersions.h"
@@ -54,11 +51,8 @@ import GHC.Types.Var.Env
import GHC.Types.Name
import GHC.Types.Unique.DFM
import GHC.Data.Maybe
-import GHC.Core.Map
-import GHC.Types.Unique
import GHC.Types.Var
import GHC.Types.SrcLoc
-import GHC.Data.FastString
import Control.Monad
import Data.List( mapAccumL )
import Data.Array( Array, assocs )
@@ -432,7 +426,7 @@ Here is how we do it:
apart(target, pattern) = not (unify(flatten(target), pattern))
where flatten (implemented in flattenTys, below) converts all type-family
-applications into fresh variables. (See Note [Flattening].)
+applications into fresh variables. (See Note [Flattening] in GHC.Core.Unify.)
Note [Compatibility]
~~~~~~~~~~~~~~~~~~~~
@@ -1179,7 +1173,7 @@ findBranch branches target_tys
, cab_incomps = incomps }) = branch
in_scope = mkInScopeSet (unionVarSets $
map (tyCoVarsOfTypes . coAxBranchLHS) incomps)
- -- See Note [Flattening] below
+ -- See Note [Flattening] in GHC.Core.Unify
flattened_target = flattenTys in_scope target_tys
in case tcMatchTys tpl_lhs target_tys of
Just subst -- matching worked. now, check for apartness.
@@ -1197,7 +1191,8 @@ findBranch branches target_tys
-- ('CoAxBranch') of a closed type family can be used to reduce a certain target
-- type family application.
apartnessCheck :: [Type] -- ^ /flattened/ target arguments. Make sure
- -- they're flattened! See Note [Flattening].
+ -- they're flattened! See Note [Flattening]
+ -- in GHC.Core.Unify
-- (NB: This "flat" is a different
-- "flat" than is used in GHC.Tc.Solver.Flatten.)
-> CoAxBranch -- ^ the candidate equation we wish to use
@@ -1563,292 +1558,3 @@ instance Monad NormM where
instance Applicative NormM where
pure x = NormM $ \ _ _ _ -> x
(<*>) = ap
-
-{-
-************************************************************************
-* *
- Flattening
-* *
-************************************************************************
-
-Note [Flattening]
-~~~~~~~~~~~~~~~~~
-As described in "Closed type families with overlapping equations"
-http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/axioms-extended.pdf
-we need to flatten core types before unifying them, when checking for "surely-apart"
-against earlier equations of a closed type family.
-Flattening means replacing all top-level uses of type functions with
-fresh variables, *taking care to preserve sharing*. That is, the type
-(Either (F a b) (F a b)) should flatten to (Either c c), never (Either
-c d).
-
-Here is a nice example of why it's all necessary:
-
- type family F a b where
- F Int Bool = Char
- F a b = Double
- type family G a -- open, no instances
-
-How do we reduce (F (G Float) (G Float))? The first equation clearly doesn't match,
-while the second equation does. But, before reducing, we must make sure that the
-target can never become (F Int Bool). Well, no matter what G Float becomes, it
-certainly won't become *both* Int and Bool, so indeed we're safe reducing
-(F (G Float) (G Float)) to Double.
-
-This is necessary not only to get more reductions (which we might be
-willing to give up on), but for substitutivity. If we have (F x x), we
-can see that (F x x) can reduce to Double. So, it had better be the
-case that (F blah blah) can reduce to Double, no matter what (blah)
-is! Flattening as done below ensures this.
-
-The algorithm works by building up a TypeMap TyVar, mapping
-type family applications to fresh variables. This mapping must
-be threaded through all the function calls, as any entry in
-the mapping must be propagated to all future nodes in the tree.
-
-The algorithm also must track the set of in-scope variables, in
-order to make fresh variables as it flattens. (We are far from a
-source of fresh Uniques.) See Wrinkle 2, below.
-
-There are wrinkles, of course:
-
-1. The flattening algorithm must account for the possibility
- of inner `forall`s. (A `forall` seen here can happen only
- because of impredicativity. However, the flattening operation
- is an algorithm in Core, which is impredicative.)
- Suppose we have (forall b. F b) -> (forall b. F b). Of course,
- those two bs are entirely unrelated, and so we should certainly
- not flatten the two calls F b to the same variable. Instead, they
- must be treated separately. We thus carry a substitution that
- freshens variables; we must apply this substitution (in
- `coreFlattenTyFamApp`) before looking up an application in the environment.
- Note that the range of the substitution contains only TyVars, never anything
- else.
-
- For the sake of efficiency, we only apply this substitution when absolutely
- necessary. Namely:
-
- * We do not perform the substitution at all if it is empty.
- * We only need to worry about the arguments of a type family that are within
- the arity of said type family, so we can get away with not applying the
- substitution to any oversaturated type family arguments.
- * Importantly, we do /not/ achieve this substitution by recursively
- flattening the arguments, as this would be wrong. Consider `F (G a)`,
- where F and G are type families. We might decide that `F (G a)` flattens
- to `beta`. Later, the substitution is non-empty (but does not map `a`) and
- so we flatten `G a` to `gamma` and try to flatten `F gamma`. Of course,
- `F gamma` is unknown, and so we flatten it to `delta`, but it really
- should have been `beta`! Argh!
-
- Moral of the story: instead of flattening the arguments, just substitute
- them directly.
-
-2. There are two different reasons we might add a variable
- to the in-scope set as we work:
-
- A. We have just invented a new flattening variable.
- B. We have entered a `forall`.
-
- Annoying here is that in-scope variable source (A) must be
- threaded through the calls. For example, consider (F b -> forall c. F c).
- Suppose that, when flattening F b, we invent a fresh variable c.
- Now, when we encounter (forall c. F c), we need to know c is already in
- scope so that we locally rename c to c'. However, if we don't thread through
- the in-scope set from one argument of (->) to the other, we won't know this
- and might get very confused.
-
- In contrast, source (B) increases only as we go deeper, as in-scope sets
- normally do. However, even here we must be careful. The TypeMap TyVar that
- contains mappings from type family applications to freshened variables will
- be threaded through both sides of (forall b. F b) -> (forall b. F b). We
- thus must make sure that the two `b`s don't get renamed to the same b1. (If
- they did, then looking up `F b1` would yield the same flatten var for
- each.) So, even though `forall`-bound variables should really be in the
- in-scope set only when they are in scope, we retain these variables even
- outside of their scope. This ensures that, if we encounter a fresh
- `forall`-bound b, we will rename it to b2, not b1. Note that keeping a
- larger in-scope set than strictly necessary is always OK, as in-scope sets
- are only ever used to avoid collisions.
-
- Sadly, the freshening substitution described in (1) really mustn't bind
- variables outside of their scope: note that its domain is the *unrenamed*
- variables. This means that the substitution gets "pushed down" (like a
- reader monad) while the in-scope set gets threaded (like a state monad).
- Because a TCvSubst contains its own in-scope set, we don't carry a TCvSubst;
- instead, we just carry a TvSubstEnv down, tying it to the InScopeSet
- traveling separately as necessary.
-
-3. Consider `F ty_1 ... ty_n`, where F is a type family with arity k:
-
- type family F ty_1 ... ty_k :: res_k
-
- It's tempting to just flatten `F ty_1 ... ty_n` to `alpha`, where alpha is a
- flattening skolem. But we must instead flatten it to
- `alpha ty_(k+1) ... ty_n`—that is, by only flattening up to the arity of the
- type family.
-
- Why is this better? Consider the following concrete example from #16995:
-
- type family Param :: Type -> Type
-
- type family LookupParam (a :: Type) :: Type where
- LookupParam (f Char) = Bool
- LookupParam x = Int
-
- foo :: LookupParam (Param ())
- foo = 42
-
- In order for `foo` to typecheck, `LookupParam (Param ())` must reduce to
- `Int`. But if we flatten `Param ()` to `alpha`, then GHC can't be sure if
- `alpha` is apart from `f Char`, so it won't fall through to the second
- equation. But since the `Param` type family has arity 0, we can instead
- flatten `Param ()` to `alpha ()`, about which GHC knows with confidence is
- apart from `f Char`, permitting the second equation to be reached.
-
- Not only does this allow more programs to be accepted, it's also important
- for correctness. Not doing this was the root cause of the Core Lint error
- in #16995.
-
-flattenTys is defined here because of module dependencies.
--}
-
-data FlattenEnv
- = FlattenEnv { fe_type_map :: TypeMap TyVar
- -- domain: exactly-saturated type family applications
- -- range: fresh variables
- , fe_in_scope :: InScopeSet }
- -- See Note [Flattening]
-
-emptyFlattenEnv :: InScopeSet -> FlattenEnv
-emptyFlattenEnv in_scope
- = FlattenEnv { fe_type_map = emptyTypeMap
- , fe_in_scope = in_scope }
-
-updateInScopeSet :: FlattenEnv -> (InScopeSet -> InScopeSet) -> FlattenEnv
-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
--- 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
-
-coreFlattenTys :: TvSubstEnv -> FlattenEnv
- -> [Type] -> (FlattenEnv, [Type])
-coreFlattenTys subst = mapAccumL (coreFlattenTy subst)
-
-coreFlattenTy :: TvSubstEnv -> FlattenEnv
- -> Type -> (FlattenEnv, Type)
-coreFlattenTy subst = go
- where
- go env ty | Just ty' <- coreView ty = go env ty'
-
- go env (TyVarTy tv)
- | Just ty <- lookupVarEnv subst tv = (env, ty)
- | otherwise = let (env', ki) = go env (tyVarKind tv) in
- (env', mkTyVarTy $ setTyVarKind tv ki)
- go env (AppTy ty1 ty2) = let (env1, ty1') = go env ty1
- (env2, ty2') = go env1 ty2 in
- (env2, AppTy ty1' ty2')
- go env (TyConApp tc tys)
- -- NB: Don't just check if isFamilyTyCon: this catches *data* families,
- -- which are generative and thus can be preserved during flattening
- | not (isGenerativeTyCon tc Nominal)
- = coreFlattenTyFamApp subst env tc tys
-
- | otherwise
- = let (env', tys') = coreFlattenTys subst env tys in
- (env', mkTyConApp tc tys')
-
- go env ty@(FunTy { ft_mult = mult, ft_arg = ty1, ft_res = ty2 })
- = let (env1, ty1') = go env ty1
- (env2, ty2') = go env1 ty2
- (env3, mult') = go env2 mult in
- (env3, ty { ft_mult = mult', ft_arg = ty1', ft_res = ty2' })
-
- go env (ForAllTy (Bndr tv vis) ty)
- = let (env1, subst', tv') = coreFlattenVarBndr subst env tv
- (env2, ty') = coreFlattenTy subst' env1 ty in
- (env2, ForAllTy (Bndr tv' vis) ty')
-
- go env ty@(LitTy {}) = (env, ty)
-
- go env (CastTy ty co)
- = let (env1, ty') = go env ty
- (env2, co') = coreFlattenCo subst env1 co in
- (env2, CastTy ty' co')
-
- go env (CoercionTy co)
- = let (env', co') = coreFlattenCo subst env co in
- (env', CoercionTy co')
-
-
--- when flattening, we don't care about the contents of coercions.
--- so, just return a fresh variable of the right (flattened) type
-coreFlattenCo :: TvSubstEnv -> FlattenEnv
- -> Coercion -> (FlattenEnv, Coercion)
-coreFlattenCo subst env co
- = (env2, mkCoVarCo covar)
- where
- (env1, kind') = coreFlattenTy subst env (coercionType co)
- covar = mkFlattenFreshCoVar (fe_in_scope env1) kind'
- -- Add the covar to the FlattenEnv's in-scope set.
- -- See Note [Flattening], wrinkle 2A.
- env2 = updateInScopeSet env1 (flip extendInScopeSet covar)
-
-coreFlattenVarBndr :: TvSubstEnv -> FlattenEnv
- -> TyCoVar -> (FlattenEnv, TvSubstEnv, TyVar)
-coreFlattenVarBndr subst env tv
- = (env2, subst', tv')
- where
- -- See Note [Flattening], wrinkle 2B.
- kind = varType tv
- (env1, kind') = coreFlattenTy subst env kind
- tv' = uniqAway (fe_in_scope env1) (setVarType tv kind')
- subst' = extendVarEnv subst tv (mkTyVarTy tv')
- env2 = updateInScopeSet env1 (flip extendInScopeSet tv')
-
-coreFlattenTyFamApp :: TvSubstEnv -> FlattenEnv
- -> TyCon -- type family tycon
- -> [Type] -- args, already flattened
- -> (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')
- where
- arity = tyConArity fam_tc
- tcv_subst = TCvSubst (fe_in_scope env) tv_subst emptyVarEnv
- (sat_fam_args, leftover_args) = ASSERT( arity <= length fam_args )
- splitAt arity fam_args
- -- Apply the substitution before looking up an application in the
- -- environment. See Note [Flattening], wrinkle 1.
- -- NB: substTys short-cuts the common case when the substitution is empty.
- sat_fam_args' = substTys tcv_subst sat_fam_args
- (env', leftover_args') = coreFlattenTys tv_subst env leftover_args
- -- `fam_tc` may be over-applied to `fam_args` (see Note [Flattening],
- -- wrinkle 3), so we split it into the arguments needed to saturate it
- -- (sat_fam_args') and the rest (leftover_args')
- fam_ty = mkTyConApp fam_tc sat_fam_args'
- FlattenEnv { fe_type_map = type_map
- , fe_in_scope = in_scope } = env'
-
-mkFlattenFreshTyName :: Uniquable a => a -> Name
-mkFlattenFreshTyName unq
- = mkSysTvName (getUnique unq) (fsLit "flt")
-
-mkFlattenFreshCoVar :: InScopeSet -> Kind -> CoVar
-mkFlattenFreshCoVar in_scope kind
- = let uniq = unsafeGetFreshLocalUnique in_scope
- name = mkSystemVarName uniq (fsLit "flc")
- in mkCoVar name kind
=====================================
compiler/GHC/Core/InstEnv.hs
=====================================
@@ -40,6 +40,7 @@ import GHC.Unit
import GHC.Core.Class
import GHC.Types.Var
import GHC.Types.Var.Set
+import GHC.Types.Var.Env
import GHC.Types.Name
import GHC.Types.Name.Set
import GHC.Types.Unique (getUnique)
@@ -827,18 +828,23 @@ lookupInstEnv' ie vis_mods cls tys
= find ms us rest
| otherwise
- = ASSERT2( tyCoVarsOfTypes tys `disjointVarSet` tpl_tv_set,
+ = ASSERT2( tys_tv_set `disjointVarSet` tpl_tv_set,
(ppr cls <+> ppr tys <+> ppr all_tvs) $$
(ppr tpl_tvs <+> ppr tpl_tys)
)
-- Unification will break badly if the variables overlap
-- They shouldn't because we allocate separate uniques for them
-- See Note [Template tyvars are fresh]
- case tcUnifyTys instanceBindFun tpl_tys tys of
- Just _ -> find ms (item:us) rest
- Nothing -> find ms us rest
+ let in_scope = mkInScopeSet (tpl_tv_set `unionVarSet` tys_tv_set)
+ flattened_tys = flattenTys in_scope tys in
+ -- NB: important to flatten here. Otherwise, it looks like
+ -- instance C Int cannot match a target [W] C (F Bool).
+ case tcUnifyTysFG instanceBindFun tpl_tys flattened_tys of
+ SurelyApart -> find ms us rest
+ _ -> find ms (item:us) rest
where
tpl_tv_set = mkVarSet tpl_tvs
+ tys_tv_set = tyCoVarsOfTypes tys
---------------
-- This is the common way to call this function.
=====================================
compiler/GHC/Core/TyCon.hs
=====================================
@@ -55,7 +55,7 @@ module GHC.Core.TyCon(
mustBeSaturated,
isPromotedDataCon, isPromotedDataCon_maybe,
isKindTyCon, isLiftedTypeKindTyConName,
- isTauTyCon, isFamFreeTyCon,
+ isTauTyCon, isFamFreeTyCon, isForgetfulSynTyCon,
isDataTyCon, isProductTyCon, isDataProductTyCon_maybe,
isDataSumTyCon_maybe,
@@ -820,10 +820,12 @@ data TyCon
synIsTau :: Bool, -- True <=> the RHS of this synonym does not
-- have any foralls, after expanding any
-- nested synonyms
- synIsFamFree :: Bool -- True <=> the RHS of this synonym does not mention
+ synIsFamFree :: Bool, -- True <=> the RHS of this synonym does not mention
-- any type synonym families (data families
-- are fine), again after expanding any
-- nested synonyms
+ synIsForgetful :: Bool -- True <=> at least one argument is not mentioned
+ -- in the RHS
}
-- | Represents families (both type and data)
@@ -1782,20 +1784,21 @@ mkPrimTyCon' name binders res_kind roles is_unlifted rep_nm
-- | Create a type synonym 'TyCon'
mkSynonymTyCon :: Name -> [TyConBinder] -> Kind -- ^ /result/ kind
- -> [Role] -> Type -> Bool -> Bool -> TyCon
-mkSynonymTyCon name binders res_kind roles rhs is_tau is_fam_free
+ -> [Role] -> Type -> Bool -> Bool -> Bool -> TyCon
+mkSynonymTyCon name binders res_kind roles rhs is_tau is_fam_free is_forgetful
= SynonymTyCon {
- tyConName = name,
- tyConUnique = nameUnique name,
- tyConBinders = binders,
- tyConResKind = res_kind,
- tyConKind = mkTyConKind binders res_kind,
- tyConArity = length binders,
- tyConTyVars = binderVars binders,
- tcRoles = roles,
- synTcRhs = rhs,
- synIsTau = is_tau,
- synIsFamFree = is_fam_free
+ tyConName = name,
+ tyConUnique = nameUnique name,
+ tyConBinders = binders,
+ tyConResKind = res_kind,
+ tyConKind = mkTyConKind binders res_kind,
+ tyConArity = length binders,
+ tyConTyVars = binderVars binders,
+ tcRoles = roles,
+ synTcRhs = rhs,
+ synIsTau = is_tau,
+ synIsFamFree = is_fam_free,
+ synIsForgetful = is_forgetful
}
-- | Create a type family 'TyCon'
@@ -2056,6 +2059,11 @@ isFamFreeTyCon (SynonymTyCon { synIsFamFree = fam_free }) = fam_free
isFamFreeTyCon (FamilyTyCon { famTcFlav = flav }) = isDataFamFlav flav
isFamFreeTyCon _ = True
+-- | Is this a forgetful type synonym?
+isForgetfulSynTyCon :: TyCon -> Bool
+isForgetfulSynTyCon (SynonymTyCon { synIsForgetful = forget }) = forget
+isForgetfulSynTyCon _ = False
+
-- As for newtypes, it is in some contexts important to distinguish between
-- closed synonyms and synonym families, as synonym families have no unique
-- right hand side to which a synonym family application can expand.
=====================================
compiler/GHC/Core/Type.hs
=====================================
@@ -1967,13 +1967,14 @@ isCoVarType ty
buildSynTyCon :: Name -> [KnotTied TyConBinder] -> Kind -- ^ /result/ kind
-> [Role] -> KnotTied Type -> TyCon
--- This function is here beucase here is where we have
+-- This function is here because here is where we have
-- isFamFree and isTauTy
buildSynTyCon name binders res_kind roles rhs
- = mkSynonymTyCon name binders res_kind roles rhs is_tau is_fam_free
+ = mkSynonymTyCon name binders res_kind roles rhs is_tau is_fam_free is_forgetful
where
- is_tau = isTauTy rhs
- is_fam_free = isFamFreeTy rhs
+ is_tau = isTauTy rhs
+ is_fam_free = isFamFreeTy rhs
+ is_forgetful = any (not . (`elemVarSet` tyCoVarsOfType rhs) . binderVar) binders
{-
************************************************************************
=====================================
compiler/GHC/Core/Unify.hs
=====================================
@@ -21,7 +21,10 @@ module GHC.Core.Unify (
UnifyResult, UnifyResultM(..),
-- Matching a type against a lifted type (coercion)
- liftCoMatch
+ liftCoMatch,
+
+ -- The core flattening algorithm
+ flattenTys
) where
#include "HsVersions.h"
@@ -31,21 +34,26 @@ import GHC.Prelude
import GHC.Types.Var
import GHC.Types.Var.Env
import GHC.Types.Var.Set
-import GHC.Types.Name( Name )
+import GHC.Types.Name( Name, mkSysTvName, mkSystemVarName )
import GHC.Core.Type hiding ( getTvSubstEnv )
import GHC.Core.Coercion hiding ( getCvSubstEnv )
import GHC.Core.TyCon
import GHC.Core.TyCo.Rep
import GHC.Core.TyCo.FVs ( tyCoVarsOfCoList, tyCoFVsOfTypes )
import GHC.Core.TyCo.Subst ( mkTvSubst )
+import GHC.Core.Map
import GHC.Utils.FV( FV, fvVarSet, fvVarList )
import GHC.Utils.Misc
import GHC.Data.Pair
import GHC.Utils.Outputable
+import GHC.Types.Unique
import GHC.Types.Unique.FM
import GHC.Types.Unique.Set
import GHC.Exts( oneShot )
+import GHC.Utils.Panic
+import GHC.Data.FastString
+import Data.List ( mapAccumL )
import Control.Monad
import Control.Applicative hiding ( empty )
import qualified Control.Applicative
@@ -691,7 +699,7 @@ unifier It does /not/ work up to ~.
The algorithm implemented here is rather delicate, and we depend on it
to uphold certain properties. This is a summary of these required
properties. Any reference to "flattening" refers to the flattening
-algorithm in GHC.Core.FamInstEnv (See Note [Flattening] in GHC.Core.FamInstEnv), not
+algorithm in GHC.Core.FamInstEnv (See Note [Flattening] in GHC.Core.Unify), not
the flattening algorithm in the solver.
Notation:
@@ -1600,3 +1608,292 @@ pushRefl co =
-> Just (ForAllCo tv (mkNomReflCo (varType tv)) (mkReflCo r ty))
-- NB: NoRefl variant. Otherwise, we get a loop!
_ -> Nothing
+
+{-
+************************************************************************
+* *
+ Flattening
+* *
+************************************************************************
+
+Note [Flattening]
+~~~~~~~~~~~~~~~~~
+As described in "Closed type families with overlapping equations"
+http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/axioms-extended.pdf
+we need to flatten core types before unifying them, when checking for "surely-apart"
+against earlier equations of a closed type family.
+Flattening means replacing all top-level uses of type functions with
+fresh variables, *taking care to preserve sharing*. That is, the type
+(Either (F a b) (F a b)) should flatten to (Either c c), never (Either
+c d).
+
+Here is a nice example of why it's all necessary:
+
+ type family F a b where
+ F Int Bool = Char
+ F a b = Double
+ type family G a -- open, no instances
+
+How do we reduce (F (G Float) (G Float))? The first equation clearly doesn't match,
+while the second equation does. But, before reducing, we must make sure that the
+target can never become (F Int Bool). Well, no matter what G Float becomes, it
+certainly won't become *both* Int and Bool, so indeed we're safe reducing
+(F (G Float) (G Float)) to Double.
+
+This is necessary not only to get more reductions (which we might be
+willing to give up on), but for substitutivity. If we have (F x x), we
+can see that (F x x) can reduce to Double. So, it had better be the
+case that (F blah blah) can reduce to Double, no matter what (blah)
+is! Flattening as done below ensures this.
+
+The algorithm works by building up a TypeMap TyVar, mapping
+type family applications to fresh variables. This mapping must
+be threaded through all the function calls, as any entry in
+the mapping must be propagated to all future nodes in the tree.
+
+The algorithm also must track the set of in-scope variables, in
+order to make fresh variables as it flattens. (We are far from a
+source of fresh Uniques.) See Wrinkle 2, below.
+
+There are wrinkles, of course:
+
+1. The flattening algorithm must account for the possibility
+ of inner `forall`s. (A `forall` seen here can happen only
+ because of impredicativity. However, the flattening operation
+ is an algorithm in Core, which is impredicative.)
+ Suppose we have (forall b. F b) -> (forall b. F b). Of course,
+ those two bs are entirely unrelated, and so we should certainly
+ not flatten the two calls F b to the same variable. Instead, they
+ must be treated separately. We thus carry a substitution that
+ freshens variables; we must apply this substitution (in
+ `coreFlattenTyFamApp`) before looking up an application in the environment.
+ Note that the range of the substitution contains only TyVars, never anything
+ else.
+
+ For the sake of efficiency, we only apply this substitution when absolutely
+ necessary. Namely:
+
+ * We do not perform the substitution at all if it is empty.
+ * We only need to worry about the arguments of a type family that are within
+ the arity of said type family, so we can get away with not applying the
+ substitution to any oversaturated type family arguments.
+ * Importantly, we do /not/ achieve this substitution by recursively
+ flattening the arguments, as this would be wrong. Consider `F (G a)`,
+ where F and G are type families. We might decide that `F (G a)` flattens
+ to `beta`. Later, the substitution is non-empty (but does not map `a`) and
+ so we flatten `G a` to `gamma` and try to flatten `F gamma`. Of course,
+ `F gamma` is unknown, and so we flatten it to `delta`, but it really
+ should have been `beta`! Argh!
+
+ Moral of the story: instead of flattening the arguments, just substitute
+ them directly.
+
+2. There are two different reasons we might add a variable
+ to the in-scope set as we work:
+
+ A. We have just invented a new flattening variable.
+ B. We have entered a `forall`.
+
+ Annoying here is that in-scope variable source (A) must be
+ threaded through the calls. For example, consider (F b -> forall c. F c).
+ Suppose that, when flattening F b, we invent a fresh variable c.
+ Now, when we encounter (forall c. F c), we need to know c is already in
+ scope so that we locally rename c to c'. However, if we don't thread through
+ the in-scope set from one argument of (->) to the other, we won't know this
+ and might get very confused.
+
+ In contrast, source (B) increases only as we go deeper, as in-scope sets
+ normally do. However, even here we must be careful. The TypeMap TyVar that
+ contains mappings from type family applications to freshened variables will
+ be threaded through both sides of (forall b. F b) -> (forall b. F b). We
+ thus must make sure that the two `b`s don't get renamed to the same b1. (If
+ they did, then looking up `F b1` would yield the same flatten var for
+ each.) So, even though `forall`-bound variables should really be in the
+ in-scope set only when they are in scope, we retain these variables even
+ outside of their scope. This ensures that, if we encounter a fresh
+ `forall`-bound b, we will rename it to b2, not b1. Note that keeping a
+ larger in-scope set than strictly necessary is always OK, as in-scope sets
+ are only ever used to avoid collisions.
+
+ Sadly, the freshening substitution described in (1) really mustn't bind
+ variables outside of their scope: note that its domain is the *unrenamed*
+ variables. This means that the substitution gets "pushed down" (like a
+ reader monad) while the in-scope set gets threaded (like a state monad).
+ Because a TCvSubst contains its own in-scope set, we don't carry a TCvSubst;
+ instead, we just carry a TvSubstEnv down, tying it to the InScopeSet
+ traveling separately as necessary.
+
+3. Consider `F ty_1 ... ty_n`, where F is a type family with arity k:
+
+ type family F ty_1 ... ty_k :: res_k
+
+ It's tempting to just flatten `F ty_1 ... ty_n` to `alpha`, where alpha is a
+ flattening skolem. But we must instead flatten it to
+ `alpha ty_(k+1) ... ty_n`—that is, by only flattening up to the arity of the
+ type family.
+
+ Why is this better? Consider the following concrete example from #16995:
+
+ type family Param :: Type -> Type
+
+ type family LookupParam (a :: Type) :: Type where
+ LookupParam (f Char) = Bool
+ LookupParam x = Int
+
+ foo :: LookupParam (Param ())
+ foo = 42
+
+ In order for `foo` to typecheck, `LookupParam (Param ())` must reduce to
+ `Int`. But if we flatten `Param ()` to `alpha`, then GHC can't be sure if
+ `alpha` is apart from `f Char`, so it won't fall through to the second
+ equation. But since the `Param` type family has arity 0, we can instead
+ flatten `Param ()` to `alpha ()`, about which GHC knows with confidence is
+ apart from `f Char`, permitting the second equation to be reached.
+
+ Not only does this allow more programs to be accepted, it's also important
+ for correctness. Not doing this was the root cause of the Core Lint error
+ in #16995.
+
+flattenTys is defined here because of module dependencies.
+-}
+
+data FlattenEnv
+ = FlattenEnv { fe_type_map :: TypeMap TyVar
+ -- domain: exactly-saturated type family applications
+ -- range: fresh variables
+ , fe_in_scope :: InScopeSet }
+ -- See Note [Flattening]
+
+emptyFlattenEnv :: InScopeSet -> FlattenEnv
+emptyFlattenEnv in_scope
+ = FlattenEnv { fe_type_map = emptyTypeMap
+ , fe_in_scope = in_scope }
+
+updateInScopeSet :: FlattenEnv -> (InScopeSet -> InScopeSet) -> FlattenEnv
+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
+-- 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
+
+coreFlattenTys :: TvSubstEnv -> FlattenEnv
+ -> [Type] -> (FlattenEnv, [Type])
+coreFlattenTys subst = mapAccumL (coreFlattenTy subst)
+
+coreFlattenTy :: TvSubstEnv -> FlattenEnv
+ -> Type -> (FlattenEnv, Type)
+coreFlattenTy subst = go
+ where
+ go env ty | Just ty' <- coreView ty = go env ty'
+
+ go env (TyVarTy tv)
+ | Just ty <- lookupVarEnv subst tv = (env, ty)
+ | otherwise = let (env', ki) = go env (tyVarKind tv) in
+ (env', mkTyVarTy $ setTyVarKind tv ki)
+ go env (AppTy ty1 ty2) = let (env1, ty1') = go env ty1
+ (env2, ty2') = go env1 ty2 in
+ (env2, AppTy ty1' ty2')
+ go env (TyConApp tc tys)
+ -- NB: Don't just check if isFamilyTyCon: this catches *data* families,
+ -- which are generative and thus can be preserved during flattening
+ | not (isGenerativeTyCon tc Nominal)
+ = coreFlattenTyFamApp subst env tc tys
+
+ | otherwise
+ = let (env', tys') = coreFlattenTys subst env tys in
+ (env', mkTyConApp tc tys')
+
+ go env ty@(FunTy { ft_mult = mult, ft_arg = ty1, ft_res = ty2 })
+ = let (env1, ty1') = go env ty1
+ (env2, ty2') = go env1 ty2
+ (env3, mult') = go env2 mult in
+ (env3, ty { ft_mult = mult', ft_arg = ty1', ft_res = ty2' })
+
+ go env (ForAllTy (Bndr tv vis) ty)
+ = let (env1, subst', tv') = coreFlattenVarBndr subst env tv
+ (env2, ty') = coreFlattenTy subst' env1 ty in
+ (env2, ForAllTy (Bndr tv' vis) ty')
+
+ go env ty@(LitTy {}) = (env, ty)
+
+ go env (CastTy ty co)
+ = let (env1, ty') = go env ty
+ (env2, co') = coreFlattenCo subst env1 co in
+ (env2, CastTy ty' co')
+
+ go env (CoercionTy co)
+ = let (env', co') = coreFlattenCo subst env co in
+ (env', CoercionTy co')
+
+
+-- when flattening, we don't care about the contents of coercions.
+-- so, just return a fresh variable of the right (flattened) type
+coreFlattenCo :: TvSubstEnv -> FlattenEnv
+ -> Coercion -> (FlattenEnv, Coercion)
+coreFlattenCo subst env co
+ = (env2, mkCoVarCo covar)
+ where
+ (env1, kind') = coreFlattenTy subst env (coercionType co)
+ covar = mkFlattenFreshCoVar (fe_in_scope env1) kind'
+ -- Add the covar to the FlattenEnv's in-scope set.
+ -- See Note [Flattening], wrinkle 2A.
+ env2 = updateInScopeSet env1 (flip extendInScopeSet covar)
+
+coreFlattenVarBndr :: TvSubstEnv -> FlattenEnv
+ -> TyCoVar -> (FlattenEnv, TvSubstEnv, TyVar)
+coreFlattenVarBndr subst env tv
+ = (env2, subst', tv')
+ where
+ -- See Note [Flattening], wrinkle 2B.
+ kind = varType tv
+ (env1, kind') = coreFlattenTy subst env kind
+ tv' = uniqAway (fe_in_scope env1) (setVarType tv kind')
+ subst' = extendVarEnv subst tv (mkTyVarTy tv')
+ env2 = updateInScopeSet env1 (flip extendInScopeSet tv')
+
+coreFlattenTyFamApp :: TvSubstEnv -> FlattenEnv
+ -> TyCon -- type family tycon
+ -> [Type] -- args, already flattened
+ -> (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')
+ where
+ arity = tyConArity fam_tc
+ tcv_subst = TCvSubst (fe_in_scope env) tv_subst emptyVarEnv
+ (sat_fam_args, leftover_args) = ASSERT( arity <= length fam_args )
+ splitAt arity fam_args
+ -- Apply the substitution before looking up an application in the
+ -- environment. See Note [Flattening], wrinkle 1.
+ -- NB: substTys short-cuts the common case when the substitution is empty.
+ sat_fam_args' = substTys tcv_subst sat_fam_args
+ (env', leftover_args') = coreFlattenTys tv_subst env leftover_args
+ -- `fam_tc` may be over-applied to `fam_args` (see Note [Flattening],
+ -- wrinkle 3), so we split it into the arguments needed to saturate it
+ -- (sat_fam_args') and the rest (leftover_args')
+ fam_ty = mkTyConApp fam_tc sat_fam_args'
+ FlattenEnv { fe_type_map = type_map
+ , fe_in_scope = in_scope } = env'
+
+mkFlattenFreshTyName :: Uniquable a => a -> Name
+mkFlattenFreshTyName unq
+ = mkSysTvName (getUnique unq) (fsLit "flt")
+
+mkFlattenFreshCoVar :: InScopeSet -> Kind -> CoVar
+mkFlattenFreshCoVar in_scope kind
+ = let uniq = unsafeGetFreshLocalUnique in_scope
+ name = mkSystemVarName uniq (fsLit "flc")
+ in mkCoVar name kind
=====================================
compiler/GHC/Tc/Errors.hs
=====================================
@@ -31,10 +31,9 @@ import GHC.Core.Type
import GHC.Core.Coercion
import GHC.Core.TyCo.Rep
import GHC.Core.TyCo.Ppr ( pprTyVars, pprWithExplicitKindsWhen, pprSourceTyCon, pprWithTYPE )
-import GHC.Core.Unify ( tcMatchTys )
+import GHC.Core.Unify ( tcMatchTys, flattenTys )
import GHC.Unit.Module
import GHC.Tc.Instance.Family
-import GHC.Core.FamInstEnv ( flattenTys )
import GHC.Tc.Utils.Instantiate
import GHC.Core.InstEnv
import GHC.Core.TyCon
=====================================
compiler/GHC/Tc/Solver/Canonical.hs
=====================================
@@ -17,7 +17,7 @@ import GHC.Prelude
import GHC.Tc.Types.Constraint
import GHC.Core.Predicate
import GHC.Tc.Types.Origin
-import GHC.Tc.Utils.Unify( swapOverTyVars, metaTyVarUpdateOK, MetaTyVarUpdateResult(..) )
+import GHC.Tc.Utils.Unify
import GHC.Tc.Utils.TcType
import GHC.Core.Type
import GHC.Tc.Solver.Flatten
@@ -2155,6 +2155,16 @@ canEqCanLHS2 ev eq_rel swapped lhs1 ps_xi1 lhs2 ps_xi2 mco
; canEqTyVarFunEq new_ev eq_rel IsSwapped tv2 ps_xi2
fun_tc1 fun_args1 ps_xi1 sym_mco }
+ | NomEq <- eq_rel
+ , TyFamLHS fun_tc1 fun_args1 <- lhs1
+ , TyFamLHS fun_tc2 fun_args2 <- lhs2
+ , fun_tc1 == fun_tc2
+ , Injective inj <- tyConInjectivityInfo fun_tc1
+ = do { traceTcS "CanEqCanLHS2 injective type family" (ppr lhs1 $$ ppr lhs2)
+ ; sequence_ [ unifyDerived (ctEvLoc ev) Nominal (Pair arg1 arg2)
+ | (arg1, arg2, True) <- zip3 fun_args1 fun_args2 inj ]
+ ; canEqCanLHSFinish ev eq_rel swapped lhs1 (ps_xi2 `mkCastTyMCo` mco) }
+
-- that's all the special cases. Now we just figure out which non-special case
-- to continue to.
| otherwise
@@ -2213,11 +2223,11 @@ canEqCanLHSFinish ev eq_rel swapped lhs rhs
-- #12593
-- guarantees (TyEq:OC), (TyEq:F), and (TyEq:H)
; case canEqOK dflags eq_rel lhs rhs of
- CanEqOK rhs' ->
- do { traceTcS "canEqOK" (ppr lhs $$ ppr rhs')
- ; new_ev <- rewriteEqEvidence ev swapped lhs_ty rhs' rewrite_co1 rewrite_co2
+ CanEqOK ->
+ do { traceTcS "canEqOK" (ppr lhs $$ ppr rhs)
+ ; new_ev <- rewriteEqEvidence ev swapped lhs_ty rhs rewrite_co1 rewrite_co2
; continueWith (CEqCan { cc_ev = new_ev, cc_lhs = lhs
- , cc_rhs = rhs', cc_eq_rel = eq_rel }) }
+ , cc_rhs = rhs, cc_eq_rel = eq_rel }) }
-- it is possible that cc_rhs mentions the LHS if the LHS is a type
-- family. This will cause later flattening to potentially loop, but
-- that will be caught by the depth counter. The other option is an
@@ -2269,11 +2279,11 @@ rewriteCastedEquality ev eq_rel swapped lhs rhs mco
-- | Result of checking whether a RHS is suitable for pairing
-- with a CanEqLHS in a CEqCan.
data CanEqOK
- = CanEqOK Xi -- use this RHS; it may have been occCheckExpand'ed
+ = CanEqOK -- RHS is good
| CanEqNotOK CtIrredStatus -- don't proceed; explains why
instance Outputable CanEqOK where
- ppr (CanEqOK rhs) = text "CanEqOK" <+> ppr rhs
+ ppr CanEqOK = text "CanEqOK"
ppr (CanEqNotOK status) = text "CanEqNotOK" <+> ppr status
-- | This function establishes most of the invariants needed to make
@@ -2287,11 +2297,9 @@ instance Outputable CanEqOK where
-- TyEq:H: Checked here.
canEqOK :: DynFlags -> EqRel -> CanEqLHS -> Xi -> CanEqOK
canEqOK dflags eq_rel lhs rhs
- | TyVarLHS tv <- lhs
- = ASSERT( good_rhs ) -- I want to put this in the pattern guard, but
- -- that confuses the pattern-match completeness checker
- case metaTyVarUpdateOK dflags True {- type families are OK here -} tv rhs of
- MTVU_OK rhs' -> CanEqOK rhs'
+ = ASSERT( good_rhs )
+ case checkTypeEq dflags True {- type families are OK here -} lhs rhs of
+ MTVU_OK () -> CanEqOK
MTVU_Bad -> CanEqNotOK OtherCIS
-- Violation of TyEq:F
@@ -2303,11 +2311,15 @@ canEqOK dflags eq_rel lhs rhs
-- These are both a violation of TyEq:OC, but we
-- want to differentiate for better production of
-- error messages
- MTVU_Occurs | isInsolubleOccursCheck eq_rel tv rhs -> CanEqNotOK InsolubleCIS
+ MTVU_Occurs | TyVarLHS tv <- lhs
+ , isInsolubleOccursCheck eq_rel tv rhs -> CanEqNotOK InsolubleCIS
-- If we have a ~ [a], it is not canonical, and in particular
-- we don't want to rewrite existing inerts with it, otherwise
-- we'd risk divergence in the constraint solver
+ -- NB: no occCheckExpand here; see Note [Flattening synonyms]
+ -- in GHC.Tc.Solver.Flatten
+
| otherwise -> CanEqNotOK OtherCIS
-- A representational equality with an occurs-check problem isn't
-- insoluble! For example:
@@ -2316,15 +2328,8 @@ canEqOK dflags eq_rel lhs rhs
-- But, the occurs-check certainly prevents the equality from being
-- canonical, and we might loop if we were to use it in rewriting.
- -- ToDo: These checks are very close to what's done in metaTyVarUpdateOK; combine?
- | TyFamLHS _fam_tc _fam_args <- lhs
- = ASSERT2( good_rhs, ppr lhs <+> dcolon <+> ppr lhs_kind $$
- ppr rhs <+> dcolon <+> ppr rhs_kind $$
- ppr eq_rel )
- if | not (isTauTy rhs) -> CanEqNotOK OtherCIS -- TyEq:F
- | badCoercionHole rhs -> CanEqNotOK BlockedCIS -- TyEq:H
- | otherwise -> CanEqOK rhs
- -- NB: TyEq:OC does not apply
+ -- This case also include type family occurs-check errors, which
+ -- are not generally insoluble
where
good_rhs = kinds_match && not bad_newtype
=====================================
compiler/GHC/Tc/Solver/Flatten.hs
=====================================
@@ -1123,16 +1123,12 @@ flatten_one (TyVarTy tv)
flatten_one (AppTy ty1 ty2)
= flatten_app_tys ty1 [ty2]
-flatten_one (TyConApp tc tys)
+flatten_one ty@(TyConApp tc tys)
-- Expand type synonyms that mention type families
-- on the RHS; see Note [Flattening synonyms]
- | Just (tenv, rhs, tys') <- expandSynTyCon_maybe tc tys
- , let expanded_ty = mkAppTys (substTy (mkTvSubstPrs tenv) rhs) tys'
- = do { mode <- getMode
- ; case mode of
- FM_FlattenAll | not (isFamFreeTyCon tc)
- -> flatten_one expanded_ty
- _ -> flatten_ty_con_app tc tys }
+ | isForgetfulSynTyCon tc
+ , Just expanded_ty <- tcView ty -- should always succeed
+ = flatten_one expanded_ty
-- Otherwise, it's a type function application, and we have to
-- flatten it away as well, and generate a new given equality constraint
@@ -1301,17 +1297,17 @@ Not expanding synonyms aggressively improves error messages, and
keeps types smaller. But we need to take care.
Suppose
- type T a = a -> a
-and we want to flatten the type (T (F a)). Then we can safely flatten
-the (F a) to a skolem, and return (T fsk). We don't need to expand the
-synonym. This works because TcTyConAppCo can deal with synonyms
-(unlike TyConAppCo), see Note [TcCoercions] in GHC.Tc.Types.Evidence.
+ type Syn a = Int
+ type instance F Bool = Syn (F Bool)
-But (#8979) for
- type T a = (F a, a) where F is a type function
-we must expand the synonym in (say) T Int, to expose the type function
-to the flattener.
+If we don't expand the synonym, we'll fall into an unnecessary loop.
+In addition, expanding the forgetful synonym like this
+will generally yield a *smaller* type. We thus expand forgetful
+synonyms, but not others.
+
+One nice consequence is that we never have to occCheckExpand flattened
+types, as any forgetful synonyms are already expanded.
Note [Flattening under a forall]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1387,20 +1383,21 @@ flatten_exact_fam_app_fully tc tys
-- Now, look in the cache
; mb_ct <- liftTcS $ lookupFlatCache tc xis
; case mb_ct of
- Just (co, rhs_ty, inert_fr) -- co :: F xis ~ fsk
+ Just (co, rhs_ty, inert_fr@(_, inert_eq_rel)) -- co :: F xis ~ fsk
-- See Note [Type family equations] in GHC.Tc.Solver.Monad
| inert_fr `eqCanRewriteFR` cur_fr
-> -- Usable hit in the flat-cache
do { traceFlat "flatten/flat-cache hit" $
(ppr tc <+> ppr xis $$ ppr rhs_ty)
- ; (fsk_xi, fsk_co) <- flatten_one rhs_ty
- -- The fsk may already have been unified, so
+ ; (rhs_xi, rhs_co) <- flatten_one rhs_ty
+ -- There may be more work to do on the rhs:
-- flatten it
- -- fsk_co :: fsk_xi ~ fsk
- ; let xi = fsk_xi `mkCastTy` kind_co
- co' = mkTcCoherenceLeftCo role fsk_xi kind_co fsk_co
+ -- rhs_co :: rhs_xi ~ rhs_ty
+ ; let xi = rhs_xi `mkCastTy` kind_co
+ co' = mkTcCoherenceLeftCo role rhs_xi kind_co rhs_co
`mkTransCo`
- maybeTcSubCo eq_rel (mkSymCo co)
+ tcDowngradeRole role (eqRelRole inert_eq_rel)
+ (mkTcSymCo co)
`mkTransCo` ret_co
; return (xi, co')
}
=====================================
compiler/GHC/Tc/Solver/Monad.hs
=====================================
@@ -407,11 +407,6 @@ data InertSet
-- flav is [G]
--
-- Just a hash-cons cache for use when flattening only
- -- These include entirely un-processed goals, so don't use
- -- them to solve a top-level goal, else you may end up solving
- -- (w:F ty ~ a) by setting w:=w! We just use the flat-cache
- -- when allocating a new flatten-skolem.
- -- Not necessarily inert wrt top-level equations (or inert_cans)
--
-- Only nominal, Given equalities end up in here (along with
-- top-level instances)
@@ -683,11 +678,11 @@ Result
data InertCans -- See Note [Detailed InertCans Invariants] for more
= IC { inert_eqs :: InertEqs
-- See Note [inert_eqs: the inert equalities]
- -- All CEqCans; index is the LHS tyvar
+ -- All CEqCans with a TyVarLHS; index is the LHS tyvar
-- Domain = skolems and untouchables; a touchable would be unified
, inert_funeqs :: FunEqMap EqualCtList
- -- All CEqCans; index is the whole family head type.
+ -- All CEqCans with a TyFamLHS; index is the whole family head type.
-- LHS is fully rewritten (modulo eqCanRewrite constraints)
-- wrt inert_eqs
-- Can include all flavours, [G], [W], [WD], [D]
@@ -3242,7 +3237,7 @@ newFlattenSkolem flav loc tc xis
= do { fmv <- wrapTcS (TcM.newFmvTyVar fam_ty)
-- See (2a) in "GHC.Tc.Solver.Canonical"
-- Note [Equalities with incompatible kinds]
- ; (ev, hole_co) <- newWantedEq_SI NoBlockSubst WDeriv loc Nominal
+ ; (ev, hole_co) <- newWantedEq_SI tcNoBlockSubst WDeriv loc Nominal
fam_ty (mkTyVarTy fmv)
; return (ev, hole_co, fmv) }
=====================================
compiler/GHC/Tc/Types/Constraint.hs
=====================================
@@ -152,7 +152,10 @@ data Ct
| CEqCan { -- tv ~ rhs
-- Invariants:
-- * See Note [inert_eqs: the inert equalities] in GHC.Tc.Solver.Monad
- -- * (TyEq:OC) if LHS is a variable tv, then tv not in deep tvs(rhs) (occurs check)
+ -- * Many are checked in checkTypeEq in GHC.Tc.Utils.Unify
+ -- * (TyEq:OC) lhs does not occur in rhs (occurs check)
+ -- (skips coercions if the lhs is a type family application, because
+ -- we don't rewrite type families in coercions)
-- * (TyEq:F) rhs has no foralls
-- (this avoids substituting a forall for the tyvar in other types)
-- * (TyEq:K) tcTypeKind lhs `tcEqKind` tcTypeKind rhs; Note [Ct kind invariant]
=====================================
compiler/GHC/Tc/Types/Evidence.hs
=====================================
@@ -134,7 +134,7 @@ mkTcForAllCo :: TyVar -> TcCoercionN -> TcCoercion -> TcCoercion
mkTcForAllCos :: [(TyVar, TcCoercionN)] -> TcCoercion -> TcCoercion
mkTcNthCo :: Role -> Int -> TcCoercion -> TcCoercion
mkTcLRCo :: LeftOrRight -> TcCoercion -> TcCoercion
-mkTcSubCo :: TcCoercionN -> TcCoercionR
+mkTcSubCo :: HasDebugCallStack => TcCoercionN -> TcCoercionR
tcDowngradeRole :: Role -> Role -> TcCoercion -> TcCoercion
mkTcAxiomRuleCo :: CoAxiomRule -> [TcCoercion] -> TcCoercionR
mkTcGReflRightCo :: Role -> TcType -> TcCoercionN -> TcCoercion
@@ -192,7 +192,7 @@ isTcReflexiveCo = isReflexiveCo
-- | If the EqRel is ReprEq, makes a SubCo; otherwise, does nothing.
-- Note that the input coercion should always be nominal.
-maybeTcSubCo :: EqRel -> TcCoercion -> TcCoercion
+maybeTcSubCo :: HasDebugCallStack => EqRel -> TcCoercionN -> TcCoercion
maybeTcSubCo NomEq = id
maybeTcSubCo ReprEq = mkTcSubCo
=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -35,7 +35,8 @@ module GHC.Tc.Utils.Unify (
matchExpectedFunKind,
matchActualFunTySigma, matchActualFunTysRho,
- metaTyVarUpdateOK, occCheckForErrors, MetaTyVarUpdateResult(..)
+ metaTyVarUpdateOK, occCheckForErrors, MetaTyVarUpdateResult(..),
+ checkTypeEq
) where
@@ -72,6 +73,7 @@ import GHC.Utils.Misc
import GHC.Utils.Outputable as Outputable
import GHC.Utils.Panic
+import GHC.Exts ( inline )
import Control.Monad
import Control.Arrow ( second )
@@ -1953,7 +1955,7 @@ occCheckForErrors :: DynFlags -> TcTyVar -> Type -> MetaTyVarUpdateResult ()
-- a) the given variable occurs in the given type.
-- b) there is a forall in the type (unless we have -XImpredicativeTypes)
occCheckForErrors dflags tv ty
- = case mtvu_check dflags True tv ty of
+ = case checkTyVarEq dflags True tv ty of
MTVU_OK _ -> MTVU_OK ()
MTVU_Bad -> MTVU_Bad
MTVU_HoleBlocker -> MTVU_HoleBlocker
@@ -1999,7 +2001,7 @@ metaTyVarUpdateOK :: DynFlags
-- See Note [Refactoring hazard: metaTyVarUpdateOK]
metaTyVarUpdateOK dflags ty_fam_ok tv ty
- = case mtvu_check dflags ty_fam_ok tv ty of
+ = case checkTyVarEq dflags ty_fam_ok tv ty of
MTVU_OK _ -> MTVU_OK ty
MTVU_Bad -> MTVU_Bad -- forall, predicate, type function
MTVU_HoleBlocker -> MTVU_HoleBlocker -- coercion hole
@@ -2007,20 +2009,31 @@ metaTyVarUpdateOK dflags ty_fam_ok tv ty
Just expanded_ty -> MTVU_OK expanded_ty
Nothing -> MTVU_Occurs
-mtvu_check :: DynFlags -> Bool -> TcTyVar -> TcType -> MetaTyVarUpdateResult ()
+checkTyVarEq :: DynFlags -> Bool -> TcTyVar -> TcType -> MetaTyVarUpdateResult ()
+checkTyVarEq dflags ty_fam_ok tv ty
+ = inline checkTypeEq dflags ty_fam_ok (TyVarLHS tv) ty
+ -- inline checkTypeEq so that the `case`s over the CanEqLHS get blasted away
+
+checkTypeEq :: DynFlags -> Bool -> CanEqLHS -> TcType -> MetaTyVarUpdateResult ()
-- Checks the invariants for CEqCan. In particular:
-- (a) a forall type (forall a. blah)
-- (b) a predicate type (c => ty)
-- (c) a type family; see Note [Prevent unification with type families]
-- (d) a blocking coercion hole
--- (e) an occurrence of the type variable (occurs check)
+-- (e) an occurrence of the LHS (occurs check)
--
-- For (a), (b), and (c) we check only the top level of the type, NOT
-- inside the kinds of variables it mentions. For (d) we look deeply
--- in coercions, and for (e) we do look in the kinds of course.
+-- in coercions when the LHS is a tyvar (but skip coercions for type family
+-- LHSs), and for (e) we do look in the kinds of course.
+--
+-- Why skip coercions for type families? Because we don't rewrite type family
+-- applications in coercions, so there's no point in looking there. On the
+-- other hand, we must check for type variables, lest we mutably create an
+-- infinite structure during unification.
-mtvu_check dflags ty_fam_ok tv ty
- = fast_check ty
+checkTypeEq dflags ty_fam_ok lhs ty
+ = go ty
where
ok :: MetaTyVarUpdateResult ()
ok = MTVU_OK ()
@@ -2029,53 +2042,75 @@ mtvu_check dflags ty_fam_ok tv ty
-- unification variables that can unify with a polytype
-- or a TyCon that would usually be disallowed by bad_tc
-- See Note [RuntimeUnkTv] in GHC.Runtime.Heap.Inspect
- ghci_tv = case tcTyVarDetails tv of
- MetaTv { mtv_info = RuntimeUnkTv } -> True
- _ -> False
-
- fast_check :: TcType -> MetaTyVarUpdateResult ()
- fast_check (TyVarTy tv')
- | tv == tv' = MTVU_Occurs
- | otherwise = fast_check_occ (tyVarKind tv')
- -- See Note [Occurrence checking: look inside kinds]
- -- in GHC.Core.Type
-
- fast_check (TyConApp tc tys)
- | bad_tc tc, not ghci_tv = MTVU_Bad
- | otherwise = mapM fast_check tys >> ok
- fast_check (LitTy {}) = ok
- fast_check (FunTy{ft_af = af, ft_mult = w, ft_arg = a, ft_res = r})
+ ghci_tv
+ | TyVarLHS tv <- lhs
+ , MetaTv { mtv_info = RuntimeUnkTv } <- tcTyVarDetails tv
+ = True
+
+ | otherwise
+ = False
+
+ go :: TcType -> MetaTyVarUpdateResult ()
+ go (TyVarTy tv') = go_tv tv'
+ go (TyConApp tc tys) = go_tc tc tys
+ go (LitTy {}) = ok
+ go (FunTy{ft_af = af, ft_mult = w, ft_arg = a, ft_res = r})
| InvisArg <- af
, not ghci_tv = MTVU_Bad
- | otherwise = fast_check w >> fast_check a >> fast_check r
- fast_check (AppTy fun arg) = fast_check fun >> fast_check arg
- fast_check (CastTy ty co) = fast_check ty >> fast_check_co co
- fast_check (CoercionTy co) = fast_check_co co
- fast_check (ForAllTy (Bndr tv' _) ty)
+ | otherwise = go w >> go a >> go r
+ go (AppTy fun arg) = go fun >> go arg
+ go (CastTy ty co) = go ty >> go_co co
+ go (CoercionTy co) = go_co co
+ go (ForAllTy (Bndr tv' _) ty)
| not ghci_tv = MTVU_Bad
- | tv == tv' = ok
- | otherwise = do { fast_check_occ (tyVarKind tv')
- ; fast_check_occ ty }
- -- Under a forall we look only for occurrences of
- -- the type variable
+ | otherwise = case lhs of
+ TyVarLHS tv | tv == tv' -> ok
+ | otherwise -> do { go_occ tv (tyVarKind tv')
+ ; go ty }
+ _ -> go ty
+
+ go_tv :: TcTyVar -> MetaTyVarUpdateResult ()
+ -- this slightly peculiar way of defining this means
+ -- we don't have to evaluate this `case` at every variable
+ -- occurrence
+ go_tv = case lhs of
+ TyVarLHS tv -> \ tv' -> if tv == tv'
+ then MTVU_Occurs
+ else go_occ tv (tyVarKind tv')
+ TyFamLHS {} -> \ _tv' -> ok
+ -- See Note [Occurrence checking: look inside kinds] in GHC.Core.Type
-- For kinds, we only do an occurs check; we do not worry
-- about type families or foralls
-- See Note [Checking for foralls]
- fast_check_occ k | tv `elemVarSet` tyCoVarsOfType k = MTVU_Occurs
- | otherwise = ok
+ go_occ tv k | tv `elemVarSet` tyCoVarsOfType k = MTVU_Occurs
+ | otherwise = ok
+
+ go_tc :: TyCon -> [TcType] -> MetaTyVarUpdateResult ()
+ -- this slightly peculiar way of defining this means
+ -- we don't have to evaluate this `case` at every tyconapp
+ go_tc = case lhs of
+ TyVarLHS {} -> \ tc tys -> if good_tc tc
+ then mapM go tys >> ok
+ else MTVU_Bad
+ TyFamLHS fam_tc fam_args -> \ tc tys ->
+ if | tcEqTyConApps fam_tc fam_args tc tys -> MTVU_Occurs
+ | good_tc tc -> mapM go tys >> ok
+ | otherwise -> MTVU_Bad
-- no bother about impredicativity in coercions, as they're
-- inferred
- fast_check_co co | not (gopt Opt_DeferTypeErrors dflags)
- , badCoercionHoleCo co = MTVU_HoleBlocker
+ go_co co | not (gopt Opt_DeferTypeErrors dflags)
+ , badCoercionHoleCo co = MTVU_HoleBlocker
-- Wrinkle (4b) in "GHC.Tc.Solver.Canonical" Note [Equalities with incompatible kinds]
- | tv `elemVarSet` tyCoVarsOfCo co = MTVU_Occurs
- | otherwise = ok
+ | TyVarLHS tv <- lhs
+ , tv `elemVarSet` tyCoVarsOfCo co = MTVU_Occurs
+ -- Don't check coercions for type families; see commentary at top of function
+ | otherwise = ok
- bad_tc :: TyCon -> Bool
- bad_tc tc
- | not (isTauTyCon tc) = True
- | not (ty_fam_ok || isFamFreeTyCon tc) = True
- | otherwise = False
+ good_tc :: TyCon -> Bool
+ good_tc
+ | ghci_tv = \ _tc -> True
+ | otherwise = \ tc -> isTauTyCon tc &&
+ (ty_fam_ok || isFamFreeTyCon tc)
=====================================
testsuite/tests/indexed-types/should_compile/T3017.stderr
=====================================
@@ -4,7 +4,7 @@ TYPE SIGNATURES
insert :: forall c. Coll c => Elem c -> c -> c
test2 ::
forall {c} {a} {b}.
- (Coll c, Num a, Num b, Elem c ~ (a, b)) =>
+ (Elem c ~ (a, b), Coll c, Num a, Num b) =>
c -> c
TYPE CONSTRUCTORS
class Coll{1} :: * -> Constraint
@@ -20,4 +20,4 @@ CLASS INSTANCES
FAMILY INSTANCES
type instance Elem (ListColl a) = a -- Defined at T3017.hs:13:9
Dependent modules: []
-Dependent packages: [base-4.13.0.0, ghc-bignum-1.0, ghc-prim-0.7.0]
+Dependent packages: [base-4.15.0.0, ghc-bignum-1.0, ghc-prim-0.7.0]
=====================================
testsuite/tests/indexed-types/should_fail/T14369.stderr
=====================================
@@ -1,9 +1,20 @@
T14369.hs:29:5: error:
- • Couldn't match type: Demote a
- with: Demote a1
+ • Couldn't match type ‘a’ with ‘a1’
Expected: Sing x -> Maybe (Demote a1)
Actual: Sing x -> Demote (Maybe a)
+ ‘a’ is a rigid type variable bound by
+ the type signature for:
+ f :: forall {a} (x :: forall a1. Maybe a1) a1.
+ SingKind a1 =>
+ Sing x -> Maybe (Demote a1)
+ at T14369.hs:28:1-80
+ ‘a1’ is a rigid type variable bound by
+ the type signature for:
+ f :: forall {a} (x :: forall a1. Maybe a1) a1.
+ SingKind a1 =>
+ Sing x -> Maybe (Demote a1)
+ at T14369.hs:28:1-80
• In the expression: fromSing
In an equation for ‘f’: f = fromSing
• Relevant bindings include
=====================================
testsuite/tests/indexed-types/should_fail/T2544.stderr
=====================================
@@ -1,13 +1,13 @@
-T2544.hs:19:18: error:
- • Couldn't match type: IxMap i0
- with: IxMap l
- Expected: IxMap l [Int]
- Actual: IxMap i0 [Int]
+T2544.hs:19:12: error:
+ • Couldn't match type: IxMap i1
+ with: IxMap r
+ Expected: IxMap (l :|: r) [Int]
+ Actual: BiApp (IxMap i0) (IxMap i1) [Int]
NB: ‘IxMap’ is a non-injective type family
- The type variable ‘i0’ is ambiguous
- • In the first argument of ‘BiApp’, namely ‘empty’
- In the expression: BiApp empty empty
+ The type variable ‘i1’ is ambiguous
+ • In the expression: BiApp empty empty
In an equation for ‘empty’: empty = BiApp empty empty
+ In the instance declaration for ‘Ix (l :|: r)’
• Relevant bindings include
empty :: IxMap (l :|: r) [Int] (bound at T2544.hs:19:4)
=====================================
testsuite/tests/indexed-types/should_fail/T2627b.stderr
=====================================
@@ -1,6 +1,6 @@
T2627b.hs:20:24: error:
- • Could not deduce: Dual (Dual b0) ~ b0
+ • Could not deduce: a0 ~ Dual (Dual a0)
arising from a use of ‘conn’
from the context: (Dual a ~ b, Dual b ~ a)
bound by the type signature for:
@@ -13,7 +13,12 @@ T2627b.hs:20:24: error:
Rd :: forall c d. (c -> Comm d) -> Comm (R c d),
in an equation for ‘conn’
at T2627b.hs:20:7-10
- The type variable ‘b0’ is ambiguous
+ or from: b ~ W e f
+ bound by a pattern with constructor:
+ Wr :: forall e f. e -> Comm f -> Comm (W e f),
+ in an equation for ‘conn’
+ at T2627b.hs:20:14-19
+ The type variable ‘a0’ is ambiguous
• In the expression: conn undefined undefined
In an equation for ‘conn’:
conn (Rd k) (Wr a r) = conn undefined undefined
=====================================
testsuite/tests/indexed-types/should_fail/T3330c.stderr
=====================================
@@ -3,14 +3,14 @@ T3330c.hs:25:43: error:
• Couldn't match kind ‘*’ with ‘* -> *’
When matching types
f1 :: * -> *
- f1 x :: *
- Expected: Der ((->) x) (f1 x)
+ Der f1 x :: *
+ Expected: Der ((->) x) (Der f1 x)
Actual: R f1
• In the first argument of ‘plug’, namely ‘rf’
In the first argument of ‘Inl’, namely ‘(plug rf df x)’
In the expression: Inl (plug rf df x)
• Relevant bindings include
x :: x (bound at T3330c.hs:25:29)
- df :: f1 x (bound at T3330c.hs:25:25)
+ df :: Der f1 x (bound at T3330c.hs:25:25)
rf :: R f1 (bound at T3330c.hs:25:13)
plug' :: R f -> Der f x -> x -> f x (bound at T3330c.hs:25:1)
=====================================
testsuite/tests/indexed-types/should_fail/T4174.stderr
=====================================
@@ -1,9 +1,9 @@
T4174.hs:44:12: error:
- • Couldn't match type ‘b’ with ‘RtsSpinLock’
+ • Couldn't match type ‘a’ with ‘SmStep’
Expected: m (Field (Way (GHC6'8 minor) n t p) a b)
Actual: m (Field (WayOf m) SmStep RtsSpinLock)
- ‘b’ is a rigid type variable bound by
+ ‘a’ is a rigid type variable bound by
the type signature for:
testcase :: forall (m :: * -> *) minor n t p a b.
Monad m =>
=====================================
testsuite/tests/indexed-types/should_fail/T4179.stderr
=====================================
@@ -1,13 +1,13 @@
T4179.hs:26:16: error:
- • Couldn't match type: A2 (x (A2 (FCon x) -> A3 (FCon x)))
- with: A2 (FCon x)
+ • Couldn't match type: A3 (FCon x)
+ with: A3 (x (A2 (FCon x) -> A3 (FCon x)))
Expected: x (A2 (FCon x) -> A3 (FCon x))
-> A2 (FCon x) -> A3 (FCon x)
Actual: x (A2 (FCon x) -> A3 (FCon x))
-> A2 (x (A2 (FCon x) -> A3 (FCon x)))
-> A3 (x (A2 (FCon x) -> A3 (FCon x)))
- NB: ‘A2’ is a non-injective type family
+ NB: ‘A3’ is a non-injective type family
• In the first argument of ‘foldDoC’, namely ‘op’
In the expression: foldDoC op
In an equation for ‘fCon’: fCon = foldDoC op
=====================================
testsuite/tests/indexed-types/should_fail/T4272.stderr
=====================================
@@ -1,17 +1,16 @@
-T4272.hs:15:26: error:
- • Couldn't match type ‘a’ with ‘TermFamily a a’
- Expected: TermFamily a (TermFamily a a)
- Actual: TermFamily a a
+T4272.hs:15:19: error:
+ • Couldn't match expected type ‘TermFamily a a’
+ with actual type ‘a’
‘a’ is a rigid type variable bound by
the type signature for:
laws :: forall a b. TermLike a => TermFamily a a -> b
at T4272.hs:14:1-53
- • In the first argument of ‘terms’, namely
- ‘(undefined :: TermFamily a a)’
- In the second argument of ‘prune’, namely
+ • In the second argument of ‘prune’, namely
‘(terms (undefined :: TermFamily a a))’
In the expression: prune t (terms (undefined :: TermFamily a a))
+ In an equation for ‘laws’:
+ laws t = prune t (terms (undefined :: TermFamily a a))
• Relevant bindings include
t :: TermFamily a a (bound at T4272.hs:15:6)
laws :: TermFamily a a -> b (bound at T4272.hs:15:1)
=====================================
testsuite/tests/indexed-types/should_fail/T5439.stderr
=====================================
@@ -30,3 +30,28 @@ T5439.hs:82:39: error:
‘inj $ Failure (e :: SomeException)’
In a stmt of a 'do' block:
c <- complete ev $ inj $ Failure (e :: SomeException)
+
+T5439.hs:245:15: error:
+ • Could not deduce: HDrop (PSucc PZero) l ~ HTail l
+ arising from a use of ‘HTailDropComm’
+ from the context: (HDropClass n l, HNonEmpty (HDrop n l))
+ bound by the type signature for:
+ hTailDropComm :: forall n l.
+ (HDropClass n l, HNonEmpty (HDrop n l)) =>
+ HTailDropComm n l
+ at T5439.hs:(242,1)-(243,34)
+ or from: (n ~ PZero, HListClass l)
+ bound by a pattern with constructor:
+ HDropZero :: forall l. HListClass l => HDropWitness PZero l,
+ in a case alternative
+ at T5439.hs:245:3-11
+ • In the expression: HTailDropComm
+ In a case alternative: HDropZero -> HTailDropComm
+ In the expression:
+ case hDropWitness :: HDropWitness n l of
+ HDropZero -> HTailDropComm
+ HDropSucc
+ -> case hTailDropComm :: HTailDropComm (PPred n) (HTail l) of {
+ HTailDropComm -> HTailDropComm }
+ • Relevant bindings include
+ hTailDropComm :: HTailDropComm n l (bound at T5439.hs:244:1)
=====================================
testsuite/tests/indexed-types/should_fail/T8227.stderr
=====================================
@@ -1,11 +1,10 @@
-T8227.hs:17:27: error:
- • Couldn't match type: Scalar (V a)
- with: Scalar (V a) -> Scalar (V a)
- Expected: Scalar (V a)
- Actual: Scalar (V (Scalar (V a) -> Scalar (V a)))
- -> Scalar (V (Scalar (V a) -> Scalar (V a)))
- • In the expression: arcLengthToParam eps eps
+T8227.hs:17:44: error:
+ • Couldn't match expected type: Scalar (V (Scalar (V a)))
+ with actual type: Scalar (V a)
+ NB: ‘Scalar’ is a non-injective type family
+ • In the first argument of ‘arcLengthToParam’, namely ‘eps’
+ In the expression: arcLengthToParam eps eps
In an equation for ‘absoluteToParam’:
absoluteToParam eps seg = arcLengthToParam eps eps
• Relevant bindings include
=====================================
testsuite/tests/indexed-types/should_fail/T8518.stderr
=====================================
@@ -1,10 +1,9 @@
T8518.hs:14:18: error:
- • Couldn't match expected type: Z c -> B c -> Maybe (F c)
- with actual type: F c
- • The function ‘rpt’ is applied to four value arguments,
- but its type ‘Int -> c -> F c’ has only two
- In the expression: rpt (4 :: Int) c z b
+ • Couldn't match type: F c
+ with: Z c -> B c -> F c
+ arising from a use of ‘rpt’
+ • In the expression: rpt (4 :: Int) c z b
In an equation for ‘callCont’:
callCont c z b
= rpt (4 :: Int) c z b
@@ -16,17 +15,3 @@ T8518.hs:14:18: error:
z :: Z c (bound at T8518.hs:14:12)
c :: c (bound at T8518.hs:14:10)
callCont :: c -> Z c -> B c -> Maybe (F c) (bound at T8518.hs:14:1)
-
-T8518.hs:16:9: error:
- • Couldn't match type: F t1
- with: Z t1 -> B t1 -> F t1
- Expected: t -> t1 -> F t1
- Actual: t -> t1 -> Z t1 -> B t1 -> F t1
- • In an equation for ‘callCont’:
- callCont c z b
- = rpt (4 :: Int) c z b
- where
- rpt 0 c' z' b' = fromJust (fst <$> (continue c' z' b'))
- rpt i c' z' b' = let ... in rpt (i - 1) c''
- • Relevant bindings include
- rpt :: t -> t1 -> F t1 (bound at T8518.hs:16:9)
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/c2972870447b7829038f7de5028e15df0ffdaf89
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/c2972870447b7829038f7de5028e15df0ffdaf89
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/20201009/96018462/attachment-0001.html>
More information about the ghc-commits
mailing list