that has one of the following two forms:
(1) co :: F t1..tn ~ t
-(2) co :: a ~ t , where t /= F t1..tn
+(2) co :: a ~ t , where t /= F t1..tn and a is a skolem tyvar
+
+NB: We do *not* use equalities of the form a ~ t where a is a meta tyvar as a
+reqrite rule. Instead, such equalities are solved by unification. This is
+essential; cf Note [skolemOccurs loop].
The following functions takes an equality instance and turns it into an
elementary rewrite if possible.
TcType -- rhs of rewrite rule
TcType -- coercion witnessing the rewrite rule
-eqInstToRewrite :: Inst -> Maybe Rewrite
+eqInstToRewrite :: Inst -> Maybe (Rewrite, Bool)
+ -- True iff rewrite swapped equality
eqInstToRewrite inst
= ASSERT( isEqInst inst )
go (eqInstLeftTy inst) (eqInstRightTy inst) (eqInstType inst)
go ty1 ty2 co | Just ty1' <- tcView ty1 = go ty1' ty2 co
go ty1 ty2 co | Just ty2' <- tcView ty2 = go ty1 ty2' co
- -- rewrite type family applications
+ -- left-to-right rule with type family head
go ty1@(TyConApp con _) ty2 co
| isOpenSynTyCon con
- = Just $ Rewrite ty1 ty2 co
+ = Just (Rewrite ty1 ty2 co, False) -- not swapped
- -- rewrite skolems
+ -- left-to-right rule with type variable head
go ty1@(TyVarTy tv) ty2 co
| isSkolemTyVar tv
- = Just $ Rewrite ty1 ty2 co
+ = Just (Rewrite ty1 ty2 co, False) -- not swapped
- -- rewrite type family applications from right-to-left, only after
+ -- right-to-left rule with type family head, only after
-- having checked whether we can work left-to-right
go ty1 ty2@(TyConApp con _) co
| isOpenSynTyCon con
- = Just $ Rewrite ty2 ty1 (mkSymCoercion co)
+ = Just (Rewrite ty2 ty1 (mkSymCoercion co), True) -- swapped
- -- rewrite skolems from right-to-left, only after having checked
- -- whether we can work left-to-right
+ -- right-to-left rule with type variable head, only after
+ -- having checked whether we can work left-to-right
go ty1 ty2@(TyVarTy tv) co
| isSkolemTyVar tv
- = Just $ Rewrite ty2 ty1 (mkSymCoercion co)
+ = Just (Rewrite ty2 ty1 (mkSymCoercion co), True) -- swapped
+ -- this equality is not a rewrite rule => ignore
go _ _ _ = Nothing
\end{code}
tcEqInstNormaliseFamInst :: Inst -> TcType -> TcM (CoercionI, TcType)
tcEqInstNormaliseFamInst inst ty
= case eqInstToRewrite inst of
- Just rewrite -> tcEqRuleNormaliseFamInst rewrite ty
- Nothing -> return (IdCo, ty)
+ Just (rewrite, _) -> tcEqRuleNormaliseFamInst rewrite ty
+ Nothing -> return (IdCo, ty)
-- Rewrite by equality rewrite rule
tcEqRuleNormaliseFamInst :: Rewrite -- elementary rewrite
F a ~ [G (F a)]
or even
- a ~ [G a]
+ a ~ [G a] , where a is a skolem tyvar
The left-to-right orientiation is not suitable because it does not
terminate. The right-to-left orientation is not suitable because it
rule doesn't need to be applied multiple times at a single inst). As a
result we can get two or more insts back.
+Note [skolemOccurs loop]
+~~~~~~~~~~~~~~~~~~~~~~~~
+You might think that under
+
+ type family F a
+ type instance F [a] = [F a]
+
+a signature such as
+
+ foo :: (F [a] ~ a) => a
+
+will get us into a loop. However, this is *not* the case. Here is why:
+
+ F [a<sk>] ~ a<sk>
+
+ -->(TOP)
+
+ [F a<sk>] ~ a<sk>
+
+ -->(SkolemOccurs)
+
+ [b<tau>] ~ a<sk>
+ F [b<tau>] ~ b<tau> , with b := F a
+
+ -->(TOP)
+
+ [b<tau>] ~ a<sk>
+ [F b<tau>] ~ b<tau> , with b := F a
+
+At this point (SkolemOccurs) does *not* apply anymore, as
+
+ [F b<tau>] ~ b<tau>
+
+is not used as a rewrite rule. The variable b<tau> is not a skolem (cf
+eqInstToRewrite).
+
+(The regression test indexed-types/should_compile/Simple20 checks that the
+described property of the system does not change.)
+
\begin{code}
skolemOccurs :: PrecondRule
skolemOccurs insts
where
oneSkolemOccurs inst
= ASSERT( isEqInst inst )
- isRewriteRule (eqInstLeftTy inst) (eqInstRightTy inst)
+ case eqInstToRewrite inst of
+ Just (rewrite, swapped) -> breakRecursion rewrite swapped
+ Nothing -> return ([inst], return ())
where
+ -- inst is an elementary rewrite rule, check whether we need to break
+ -- it up
+ breakRecursion (Rewrite pat body _) swapped
- -- look through synonyms
- isRewriteRule ty1 ty2 | Just ty1' <- tcView ty1 = isRewriteRule ty1' ty2
- isRewriteRule ty1 ty2 | Just ty2' <- tcView ty2 = isRewriteRule ty1 ty2'
-
- -- left-to-right rule with type family head
- isRewriteRule ty1@(TyConApp con _) ty2
- | isOpenSynTyCon con
- = breakRecursion ty1 ty2 False -- not swapped
-
- -- left-to-right rule with type variable head
- isRewriteRule ty1@(TyVarTy _) ty2
- = breakRecursion ty1 ty2 False -- not swapped
-
- -- right-to-left rule with type family head
- isRewriteRule ty1 ty2@(TyConApp con _)
- | isOpenSynTyCon con
- = breakRecursion ty2 ty1 True -- swapped
-
- -- right-to-left rule with type variable head
- isRewriteRule ty1 ty2@(TyVarTy _)
- = breakRecursion ty2 ty1 True -- swapped
-
- -- this equality is not a rewrite rule => ignore
- isRewriteRule _ _ = return ([inst], return ())
-
- ------------------
- breakRecursion pat body swapped
+ -- skolemOccurs does not apply, leave as is
| null tysToLiftOut
- = return ([inst], return ())
+ = do { traceTc $ text "oneSkolemOccurs: no tys to lift out"
+ ; return ([inst], return ())
+ }
+
+ -- recursive occurence of pat in body under a type family application
| otherwise
= do { traceTc $ text "oneSkolemOccurs[TLO]:" <+> ppr tysToLiftOut
; skTvs <- mapM (newMetaTyVar TauTv . typeKind) tysToLiftOut
substInst :: Inst -> [Inst] -> TcM ([Inst], Bool)
substInst inst insts
= case eqInstToRewrite inst of
- Just rewrite -> substEquality rewrite insts
- Nothing -> return (insts, False)
+ Just (rewrite, _) -> substEquality rewrite insts
+ Nothing -> return (insts, False)
where
substEquality :: Rewrite -- elementary rewrite
-> [Inst] -- insts to rewrite
-- (ppr_extra env ty) shows extra info about 'ty'
ppr_extra :: TidyEnv -> Type -> TcM (TidyEnv, SDoc)
ppr_extra env (TyVarTy tv)
- | isSkolemTyVar tv || isSigTyVar tv
+ | isTcTyVar tv && (isSkolemTyVar tv || isSigTyVar tv)
= return (env1, pprSkolTvBinding tv1)
where
(env1, tv1) = tidySkolemTyVar env tv
projects / ghc-hetmet.git / blobdiff