substEqInDictInsts,
-- errors
- eqInstMisMatch, misMatchMsg,
+ misMatchMsg, failWithMisMatch
) where
tcNormaliseFamInstPred = tcGenericNormaliseFamInstPred tcUnfoldSynFamInst
\end{code}
-Normalise a type relative to the rewrite rule implied by one EqInst or an
-already unpacked EqInst (ie, an equality rewrite rule).
+An elementary rewrite is a properly oriented equality with associated coercion
+that has one of the following two forms:
+
+(1) co :: F t1..tn ~ t
+(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.
\begin{code}
--- Rewrite by EqInst
-tcEqInstNormaliseFamInst :: Inst -> TcType -> TcM (CoercionI, Type)
-tcEqInstNormaliseFamInst inst =
- ASSERT( isEqInst inst )
- tcEqRuleNormaliseFamInst (pat, rhs, co)
+data Rewrite = Rewrite TcType -- lhs of rewrite rule
+ TcType -- rhs of rewrite rule
+ TcType -- coercion witnessing the rewrite rule
+
+eqInstToRewrite :: Inst -> Maybe (Rewrite, Bool)
+ -- True iff rewrite swapped equality
+eqInstToRewrite inst
+ = ASSERT( isEqInst inst )
+ go ty1 ty2 (eqInstType inst)
where
- pat = eqInstLeftTy inst
- rhs = eqInstRightTy inst
- co = eqInstType inst
+ (ty1,ty2) = eqInstTys inst
+
+ -- look through synonyms
+ go ty1 ty2 co | Just ty1' <- tcView ty1 = go ty1' ty2 co
+ go ty1 ty2 co | Just ty2' <- tcView ty2 = go ty1 ty2' co
+
+ -- left-to-right rule with type family head
+ go ty1@(TyConApp con _) ty2 co
+ | isOpenSynTyCon con
+ = Just (Rewrite ty1 ty2 co, False) -- not swapped
+
+ -- left-to-right rule with type variable head
+ go ty1@(TyVarTy tv) ty2 co
+ | isSkolemTyVar tv
+ = Just (Rewrite ty1 ty2 co, False) -- not swapped
+
+ -- 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), True) -- swapped
+
+ -- 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), True) -- swapped
+
+ -- this equality is not a rewrite rule => ignore
+ go _ _ _ = Nothing
+\end{code}
+
+Normalise a type relative to an elementary rewrite implied by an EqInst or an
+explicitly given elementary rewrite.
+
+\begin{code}
+-- Rewrite by EqInst
+-- Precondition: the EqInst passes the occurs check
+tcEqInstNormaliseFamInst :: Inst -> TcType -> TcM (CoercionI, TcType)
+tcEqInstNormaliseFamInst inst ty
+ = case eqInstToRewrite inst of
+ Just (rewrite, _) -> tcEqRuleNormaliseFamInst rewrite ty
+ Nothing -> return (IdCo, ty)
-- Rewrite by equality rewrite rule
-tcEqRuleNormaliseFamInst :: (TcType, -- rewrite rule lhs
- TcType, -- rewrite rule rhs
- TcType) -- coercion witnessing the rewrite rule
- -> TcType -- type to rewrite
- -> TcM (CoercionI, Type)
-tcEqRuleNormaliseFamInst (pat, rhs, co) ty
+tcEqRuleNormaliseFamInst :: Rewrite -- elementary rewrite
+ -> TcType -- type to rewrite
+ -> TcM (CoercionI, -- witnessing coercion
+ TcType) -- rewritten type
+tcEqRuleNormaliseFamInst (Rewrite pat rhs co) ty
= tcGenericNormaliseFamInst matchEqRule ty
where
matchEqRule sty | pat `tcEqType` sty = return $ Just (rhs, co)
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 { skTvs <- mapM (newMetaTyVar TauTv . typeKind) tysToLiftOut
+ = do { traceTc $ text "oneSkolemOccurs[TLO]:" <+> ppr tysToLiftOut
+ ; skTvs <- mapM (newMetaTyVar TauTv . typeKind) tysToLiftOut
; let skTvs_tysTLO = zip skTvs tysToLiftOut
insertSkolems = return . replace skTvs_tysTLO
; (_, body') <- tcGenericNormaliseFamInst insertSkolems body
else mkEqInst (EqPred pat body') co
-- ensure to reconstruct the inst in the
-- original orientation
+ ; traceTc $ text "oneSkolemOccurs[inst']:" <+> ppr inst'
; (insts, undoSk) <- mapAndUnzipM (mkSkolemInst inst')
skTvs_tysTLO
; return (inst':insts, sequence_ undoSk)
= do { (co, tyLiftedOut) <- tcEqInstNormaliseFamInst inst' tyTLO
; inst <- mkEqInst (EqPred tyLiftedOut (mkTyVarTy skTv))
(mkGivenCo $ mkSymCoercion (fromACo co))
+ -- co /= IdCo due to construction of inst'
; return (inst, writeMetaTyVar skTv tyTLO)
}
\end{code}
| otherwise
= return $ Just inst
where
- ty1 = eqInstLeftTy inst
- ty2 = eqInstRightTy inst
+ (ty1,ty2) = eqInstTys inst
\end{code}
where
decomp inst
= ASSERT( isEqInst inst )
- go (eqInstLeftTy inst) (eqInstRightTy inst)
+ go ty1 ty2
where
+ (ty1,ty2) = eqInstTys inst
go ty1 ty2
| Just ty1' <- tcView ty1 = go ty1' ty2
| Just ty2' <- tcView ty2 = go ty1 ty2'
}
}
where
- ty1 = eqInstLeftTy inst
- ty2 = eqInstRightTy inst
+ (ty1,ty2) = eqInstTys inst
\end{code}
--
substInst :: Inst -> [Inst] -> TcM ([Inst], Bool)
substInst inst insts
- = ASSERT( isEqInst inst )
- go (eqInstLeftTy inst) (eqInstRightTy inst) (eqInstType inst)
+ = case eqInstToRewrite inst of
+ Just (rewrite, _) -> substEquality rewrite insts
+ Nothing -> return (insts, False)
where
- -- look through synonyms
- 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
- go ty1@(TyConApp con _) ty2 co
- | isOpenSynTyCon con
- = substEquality (ty1, ty2, co) insts
-
- -- rewrite skolems
- go ty1@(TyVarTy tv) ty2 co
- | isSkolemTyVar tv
- = substEquality (ty1, ty2, co) insts
-
- -- rewrite type family applications from right-to-left, only after
- -- having checked whether we can work left-to-right
- go ty1 ty2@(TyConApp con _) co
- | isOpenSynTyCon con
- = substEquality (ty2, ty1, mkSymCoercion co) insts
-
- -- rewrite skolems from right-to-left, only after having checked
- -- whether we can work left-to-right
- go ty1 ty2@(TyVarTy tv) co
- | isSkolemTyVar tv
- = substEquality (ty2, ty1, mkSymCoercion co) insts
-
- go _ _ _ = return (insts, False)
-
- substEquality :: (TcType, -- rewrite rule lhs
- TcType, -- rewrite rule rhs
- TcType) -- coercion witnessing the rewrite rule
- -> [Inst] -- insts to rewrite
+ substEquality :: Rewrite -- elementary rewrite
+ -> [Inst] -- insts to rewrite
-> TcM ([Inst], Bool)
- substEquality eqRule@(pat, rhs, _) insts
+ substEquality eqRule@(Rewrite pat rhs _) insts
| pat `tcPartOfType` rhs -- occurs check!
= occurCheckErr pat rhs
| otherwise
}
}
where
- ty1 = eqInstLeftTy inst
- ty2 = eqInstRightTy inst
+ (ty1,ty2) = eqInstTys inst
\end{code}
where
unifyMeta inst
= ASSERT( isEqInst inst )
- go (eqInstLeftTy inst) (eqInstRightTy inst)
+ go ty1 ty2
(fromWantedCo "unifyMetaRule" $ eqInstCoercion inst)
where
+ (ty1,ty2) = eqInstTys inst
go ty1 ty2 cotv
| Just ty1' <- tcView ty1 = go ty1' ty2 cotv
| Just ty2' <- tcView ty2 = go ty1 ty2' cotv
-- updatable meta variable meets non-variable type
-- => occurs check, monotype check, and kinds match check, then update
uMeta swapped tv (DoneTv (MetaTv _ ref)) ty cotv
- = do { ty' <- checkTauTvUpdate tv ty -- occurs + monotype check
- ; checkUpdateMeta swapped tv ref ty' -- update meta var
- ; writeMetaTyVar cotv ty' -- update the co var
- ; return ([], True)
+ = do { mb_ty' <- checkTauTvUpdate tv ty -- occurs + monotype check
+ ; case mb_ty' of
+ Nothing -> return ([inst], False) -- tv occurs in faminst
+ Just ty' ->
+ do { checkUpdateMeta swapped tv ref ty' -- update meta var
+ ; writeMetaTyVar cotv ty' -- update co var
+ ; return ([], True)
+ }
}
uMeta _ _ _ _ _ = panic "uMeta"
eqInstMisMatch :: Inst -> TcM a
eqInstMisMatch inst
= ASSERT( isEqInst inst )
- do { (env, msg) <- misMatchMsg ty_act ty_exp
- ; setErrCtxt ctxt $
- failWithTcM (env, msg)
- }
+ setErrCtxt ctxt $ failWithMisMatch ty_act ty_exp
where
- ty_act = eqInstLeftTy inst
- ty_exp = eqInstRightTy inst
- InstLoc _ _ ctxt = instLoc inst
+ (ty_act, ty_exp) = eqInstTys inst
+ InstLoc _ _ ctxt = instLoc inst
-----------------------
-misMatchMsg :: TcType -> TcType -> TcM (TidyEnv, SDoc)
+failWithMisMatch :: TcType -> TcType -> TcM a
-- Generate the message when two types fail to match,
-- going to some trouble to make it helpful.
-- The argument order is: actual type, expected type
-misMatchMsg ty_act ty_exp
+failWithMisMatch ty_act ty_exp
= do { env0 <- tcInitTidyEnv
; ty_exp <- zonkTcType ty_exp
; ty_act <- zonkTcType ty_act
- ; (env1, pp_exp, extra_exp) <- ppr_ty env0 ty_exp
- ; (env2, pp_act, extra_act) <- ppr_ty env1 ty_act
- ; return (env2,
- sep [sep [ptext SLIT("Couldn't match expected type") <+> pp_exp,
- nest 7 $
+ ; failWithTcM (misMatchMsg env0 (ty_act, ty_exp))
+ }
+
+misMatchMsg :: TidyEnv -> (TcType, TcType) -> (TidyEnv, SDoc)
+misMatchMsg env0 (ty_act, ty_exp)
+ = let (env1, pp_exp, extra_exp) = ppr_ty env0 ty_exp
+ (env2, pp_act, extra_act) = ppr_ty env1 ty_act
+ msg = sep [sep [ptext SLIT("Couldn't match expected type") <+> pp_exp,
+ nest 7 $
ptext SLIT("against inferred type") <+> pp_act],
- nest 2 (extra_exp $$ extra_act)]) }
-
-ppr_ty :: TidyEnv -> TcType -> TcM (TidyEnv, SDoc, SDoc)
-ppr_ty env ty
- = do { let (env1, tidy_ty) = tidyOpenType env ty
- ; (env2, extra) <- ppr_extra env1 tidy_ty
- ; return (env2, quotes (ppr tidy_ty), extra) }
-
--- (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
- = return (env1, pprSkolTvBinding tv1)
+ nest 2 (extra_exp $$ extra_act)]
+ in
+ (env2, msg)
+
where
- (env1, tv1) = tidySkolemTyVar env tv
+ ppr_ty :: TidyEnv -> TcType -> (TidyEnv, SDoc, SDoc)
+ ppr_ty env ty
+ = let (env1, tidy_ty) = tidyOpenType env ty
+ (env2, extra) = ppr_extra env1 tidy_ty
+ in
+ (env2, quotes (ppr tidy_ty), extra)
+
+ -- (ppr_extra env ty) shows extra info about 'ty'
+ ppr_extra :: TidyEnv -> Type -> (TidyEnv, SDoc)
+ ppr_extra env (TyVarTy tv)
+ | isTcTyVar tv && (isSkolemTyVar tv || isSigTyVar tv) && not (isUnk tv)
+ = (env1, pprSkolTvBinding tv1)
+ where
+ (env1, tv1) = tidySkolemTyVar env tv
-ppr_extra env _ty = return (env, empty) -- Normal case
+ ppr_extra env _ty = (env, empty) -- Normal case
\end{code}
projects / ghc-hetmet.git / blobdiff