module TcUnify (
-- Full-blown subsumption
- tcSubExp, tcFunResTy, tcGen,
+ tcSubExp, tcGen,
checkSigTyVars, checkSigTyVarsWrt, bleatEscapedTvs, sigCtxt,
-- Various unifications
import Util
import Outputable
import Unique
+import FastString
+
+import Control.Monad
\end{code}
%************************************************************************
\begin{code}
tcInfer :: (BoxyType -> TcM a) -> TcM (a, TcType)
-tcInfer tc_infer
- = do { box <- newBoxyTyVar openTypeKind
- ; res <- tc_infer (mkTyVarTy box)
- ; res_ty <- {- pprTrace "tcInfer" (ppr (mkTyVarTy box)) $ -} readFilledBox box -- Guaranteed filled-in by now
- ; return (res, res_ty) }
+tcInfer tc_infer = withBox openTypeKind tc_infer
\end{code}
loop n args_so_far res_ty = bale_out args_so_far
- -- build a template type a1 -> ... -> an -> b and defer an equality
+ -- Build a template type a1 -> ... -> an -> b and defer an equality
-- between that template and the expected result type res_ty; then,
-- use the template to type the thing_inside
defer n args_so_far ty
err = error_herald <> comma $$
text "which does not match its type"
; coi <- addErrCtxt err $
- defer_unification False False fun_ty ty
+ defer_unification (Unify False fun_ty ty) False fun_ty ty
; res <- thing_inside (reverse args_so_far ++ arg_tys) res_ty'
; return (coiToHsWrapper coi, res)
}
boxySplitTyConApp :: TyCon -- T :: k1 -> ... -> kn -> *
-> BoxyRhoType -- Expected type (T a b c)
-> TcM ([BoxySigmaType], -- Element types, a b c
- CoercionI)
+ CoercionI) -- T a b c ~ orig_ty
-- It's used for wired-in tycons, so we call checkWiredInTyCon
-- Precondition: never called with FunTyCon
-- Precondition: input type :: *
| Just (fun_ty, arg_ty) <- tcSplitAppTy_maybe ty
= return ((fun_ty, arg_ty), IdCo)
- loop ty@(TyConApp tycon args)
+ loop ty@(TyConApp tycon _args)
| isOpenSynTyCon tycon -- try to normalise type family application
= do { (coi1, ty') <- tcNormaliseFamInst ty
; case coi1 of
mk_res_ty _other = panic "TcUnify.mk_res_ty2"
------------------
-boxySplitFailure actual_ty expected_ty
- = unifyMisMatch False False actual_ty expected_ty
- -- "outer" is False, so we don't pop the context
- -- which is what we want since we have not pushed one!
+boxySplitFailure actual_ty expected_ty = failWithMisMatch actual_ty expected_ty
------------------
boxySplitDefer :: [Kind] -- kinds of required arguments
-> ([TcType] -> TcTauType) -- construct lhs from argument tyvars
-> BoxyRhoType -- type to split
-> TcM ([TcType], CoercionI)
-boxySplitDefer kinds mkTy orig_ty
+boxySplitDefer kinds mk_ty orig_ty
= do { tau_tys <- mapM newFlexiTyVarTy kinds
- ; coi <- defer_unification False False (mkTy tau_tys) orig_ty
+ ; let ty1 = mk_ty tau_tys
+ ; coi <- defer_unification (Unify False ty1 orig_ty) False ty1 orig_ty
; return (tau_tys, coi)
}
\end{code}
withBox :: Kind -> (BoxySigmaType -> TcM a) -> TcM (a, TcType)
-- Allocate a *boxy* tyvar
withBox kind thing_inside
- = do { box_tv <- newMetaTyVar BoxTv kind
+ = do { box_tv <- newBoxyTyVar kind
; res <- thing_inside (mkTyVarTy box_tv)
; ty <- {- pprTrace "with_box" (ppr (mkTyVarTy box_tv)) $ -} readFilledBox box_tv
; return (res, ty) }
Nothing -> orig_boxy_ty
Just ty -> ty `boxyLub` orig_boxy_ty
+ go _ (TyVarTy tv) | isMetaTyVar tv
+ = subst -- Don't fail if the template has more info than the target!
+ -- Otherwise, with tmpl_tvs = [a], matching (a -> Int) ~ (Bool -> beta)
+ -- would fail to instantiate 'a', because the meta-type-variable
+ -- beta is as yet un-filled-in
+
go _ _ = emptyTvSubst -- It's important to *fail* by returning the empty substitution
-- Example: Tree a ~ Maybe Int
-- We do not want to bind (a |-> Int) in pre-matching, because that can give very
| isTcTyVar tv1, isBoxyTyVar tv1 -- choose ty2 if ty2 is a box
= orig_ty2
+ go ty1 (TyVarTy tv2) -- Symmetrical case
+ | isTcTyVar tv2, isBoxyTyVar tv2
+ = orig_ty1
+
-- Look inside type synonyms, but only if the naive version fails
go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2
| Just ty2' <- tcView ty1 = go ty1 ty2'
All the tcSub calls have the form
- tcSub expected_ty offered_ty
+ tcSub actual_ty expected_ty
which checks
- offered_ty <= expected_ty
+ actual_ty <= expected_ty
-That is, that a value of type offered_ty is acceptable in
+That is, that a value of type actual_ty is acceptable in
a place expecting a value of type expected_ty.
It returns a coercion function
- co_fn :: offered_ty ~ expected_ty
-which takes an HsExpr of type offered_ty into one of type
+ co_fn :: actual_ty ~ expected_ty
+which takes an HsExpr of type actual_ty into one of type
expected_ty.
\begin{code}
-----------------
-tcSubExp :: BoxySigmaType -> BoxySigmaType -> TcM HsWrapper -- Locally used only
+tcSubExp :: InstOrigin -> BoxySigmaType -> BoxySigmaType -> TcM HsWrapper
-- (tcSub act exp) checks that
-- act <= exp
-tcSubExp actual_ty expected_ty
+tcSubExp orig actual_ty expected_ty
= -- addErrCtxtM (unifyCtxt actual_ty expected_ty) $
-- Adding the error context here leads to some very confusing error
-- messages, such as "can't match forall a. a->a with forall a. a->a"
-- So instead I'm adding the error context when moving from tc_sub to u_tys
traceTc (text "tcSubExp" <+> ppr actual_ty <+> ppr expected_ty) >>
- tc_sub SubOther actual_ty actual_ty False expected_ty expected_ty
+ tc_sub orig actual_ty actual_ty False expected_ty expected_ty
-tcFunResTy :: Name -> BoxySigmaType -> BoxySigmaType -> TcM HsWrapper -- Locally used only
-tcFunResTy fun actual_ty expected_ty
- = traceTc (text "tcFunResTy" <+> ppr actual_ty <+> ppr expected_ty) >>
- tc_sub (SubFun fun) actual_ty actual_ty False expected_ty expected_ty
-
-----------------
-data SubCtxt = SubDone -- Error-context already pushed
- | SubFun Name -- Context is tcFunResTy
- | SubOther -- Context is something else
-
-tc_sub :: SubCtxt -- How to add an error-context
+tc_sub :: InstOrigin
-> BoxySigmaType -- actual_ty, before expanding synonyms
-> BoxySigmaType -- ..and after
-> InBox -- True <=> expected_ty is inside a box
-- This invariant is needed so that we can "see" the foralls, ad
-- e.g. in the SPEC rule where we just use splitSigmaTy
-tc_sub sub_ctxt act_sty act_ty exp_ib exp_sty exp_ty
+tc_sub orig act_sty act_ty exp_ib exp_sty exp_ty
= traceTc (text "tc_sub" <+> ppr act_ty $$ ppr exp_ty) >>
- tc_sub1 sub_ctxt act_sty act_ty exp_ib exp_sty exp_ty
+ tc_sub1 orig act_sty act_ty exp_ib exp_sty exp_ty
-- This indirection is just here to make
-- it easy to insert a debug trace!
-tc_sub1 sub_ctxt act_sty act_ty exp_ib exp_sty exp_ty
- | Just exp_ty' <- tcView exp_ty = tc_sub sub_ctxt act_sty act_ty exp_ib exp_sty exp_ty'
-tc_sub1 sub_ctxt act_sty act_ty exp_ib exp_sty exp_ty
- | Just act_ty' <- tcView act_ty = tc_sub sub_ctxt act_sty act_ty' exp_ib exp_sty exp_ty
+tc_sub1 orig act_sty act_ty exp_ib exp_sty exp_ty
+ | Just exp_ty' <- tcView exp_ty = tc_sub orig act_sty act_ty exp_ib exp_sty exp_ty'
+tc_sub1 orig act_sty act_ty exp_ib exp_sty exp_ty
+ | Just act_ty' <- tcView act_ty = tc_sub orig act_sty act_ty' exp_ib exp_sty exp_ty
-----------------------------------
-- Rule SBOXY, plus other cases when act_ty is a type variable
-- Just defer to boxy matching
-- This rule takes precedence over SKOL!
-tc_sub1 sub_ctxt act_sty (TyVarTy tv) exp_ib exp_sty exp_ty
+tc_sub1 orig act_sty (TyVarTy tv) exp_ib exp_sty exp_ty
= do { traceTc (text "tc_sub1 - case 1")
- ; coi <- addSubCtxt sub_ctxt act_sty exp_sty $
- uVar True False tv exp_ib exp_sty exp_ty
+ ; coi <- addSubCtxt orig act_sty exp_sty $
+ uVar (Unify True act_sty exp_sty) False tv exp_ib exp_sty exp_ty
; traceTc (case coi of
IdCo -> text "tc_sub1 (Rule SBOXY) IdCo"
ACo co -> text "tc_sub1 (Rule SBOXY) ACo" <+> ppr co)
-- g :: Ord b => b->b
-- Consider f g !
-tc_sub1 sub_ctxt act_sty act_ty exp_ib exp_sty exp_ty
- | isSigmaTy exp_ty
- = do { traceTc (text "tc_sub1 - case 2") ;
+tc_sub1 orig act_sty act_ty exp_ib exp_sty exp_ty
+ | isSigmaTy exp_ty = do
+ { traceTc (text "tc_sub1 - case 2") ;
if exp_ib then -- SKOL does not apply if exp_ty is inside a box
- defer_to_boxy_matching sub_ctxt act_sty act_ty exp_ib exp_sty exp_ty
+ defer_to_boxy_matching orig act_sty act_ty exp_ib exp_sty exp_ty
else do
{ (gen_fn, co_fn) <- tcGen exp_ty act_tvs $ \ _ body_exp_ty ->
- tc_sub sub_ctxt act_sty act_ty False body_exp_ty body_exp_ty
+ tc_sub orig act_sty act_ty False body_exp_ty body_exp_ty
; return (gen_fn <.> co_fn) }
}
where
-- expected_ty: Int -> Int
-- co_fn e = e Int dOrdInt
-tc_sub1 sub_ctxt act_sty actual_ty exp_ib exp_sty expected_ty
+tc_sub1 orig act_sty actual_ty exp_ib exp_sty expected_ty
-- Implements the new SPEC rule in the Appendix of the paper
-- "Boxy types: inference for higher rank types and impredicativity"
-- (This appendix isn't in the published version.)
; traceTc (text "tc_sub_spec" <+> vcat [ppr actual_ty,
ppr tyvars <+> ppr theta <+> ppr tau,
ppr tau'])
- ; co_fn2 <- tc_sub sub_ctxt tau' tau' exp_ib exp_sty expected_ty
+ ; co_fn2 <- tc_sub orig tau' tau' exp_ib exp_sty expected_ty
-- Deal with the dictionaries
- -- The origin gives a helpful origin when we have
- -- a function with type f :: Int -> forall a. Num a => ...
- -- This way the (Num a) dictionary gets an OccurrenceOf f origin
- ; let orig = case sub_ctxt of
- SubFun n -> OccurrenceOf n
- other -> InstSigOrigin -- Unhelpful
; co_fn1 <- instCall orig inst_tys (substTheta subst' theta)
; return (co_fn2 <.> co_fn1) }
-----------------------------------
-- Function case (rule F1)
-tc_sub1 sub_ctxt act_sty (FunTy act_arg act_res) exp_ib exp_sty (FunTy exp_arg exp_res)
+tc_sub1 orig act_sty (FunTy act_arg act_res) exp_ib exp_sty (FunTy exp_arg exp_res)
= do { traceTc (text "tc_sub1 - case 4")
- ; addSubCtxt sub_ctxt act_sty exp_sty $
- tc_sub_funs act_arg act_res exp_ib exp_arg exp_res
+ ; tc_sub_funs orig act_arg act_res exp_ib exp_arg exp_res
}
-- Function case (rule F2)
-tc_sub1 sub_ctxt act_sty act_ty@(FunTy act_arg act_res) _ exp_sty (TyVarTy exp_tv)
+tc_sub1 orig act_sty act_ty@(FunTy act_arg act_res) _ exp_sty (TyVarTy exp_tv)
| isBoxyTyVar exp_tv
- = addSubCtxt sub_ctxt act_sty exp_sty $
- do { traceTc (text "tc_sub1 - case 5")
+ = do { traceTc (text "tc_sub1 - case 5")
; cts <- readMetaTyVar exp_tv
; case cts of
- Indirect ty -> tc_sub SubDone act_sty act_ty True exp_sty ty
+ Indirect ty -> tc_sub orig act_sty act_ty True exp_sty ty
Flexi -> do { [arg_ty,res_ty] <- withMetaTvs exp_tv fun_kinds mk_res_ty
- ; tc_sub_funs act_arg act_res True arg_ty res_ty } }
+ ; tc_sub_funs orig act_arg act_res True arg_ty res_ty } }
where
mk_res_ty [arg_ty', res_ty'] = mkFunTy arg_ty' res_ty'
mk_res_ty other = panic "TcUnify.mk_res_ty3"
fun_kinds = [argTypeKind, openTypeKind]
-- Everything else: defer to boxy matching
-tc_sub1 sub_ctxt act_sty actual_ty exp_ib exp_sty expected_ty@(TyVarTy exp_tv)
+tc_sub1 orig act_sty actual_ty exp_ib exp_sty expected_ty@(TyVarTy exp_tv)
= do { traceTc (text "tc_sub1 - case 6a" <+> ppr [isBoxyTyVar exp_tv, isMetaTyVar exp_tv, isSkolemTyVar exp_tv, isExistentialTyVar exp_tv,isSigTyVar exp_tv] )
- ; defer_to_boxy_matching sub_ctxt act_sty actual_ty exp_ib exp_sty expected_ty
+ ; defer_to_boxy_matching orig act_sty actual_ty exp_ib exp_sty expected_ty
}
-tc_sub1 sub_ctxt act_sty actual_ty exp_ib exp_sty expected_ty
+tc_sub1 orig act_sty actual_ty exp_ib exp_sty expected_ty
= do { traceTc (text "tc_sub1 - case 6")
- ; defer_to_boxy_matching sub_ctxt act_sty actual_ty exp_ib exp_sty expected_ty
+ ; defer_to_boxy_matching orig act_sty actual_ty exp_ib exp_sty expected_ty
}
-----------------------------------
-defer_to_boxy_matching sub_ctxt act_sty actual_ty exp_ib exp_sty expected_ty
- = do { coi <- addSubCtxt sub_ctxt act_sty exp_sty $
- u_tys outer False act_sty actual_ty exp_ib exp_sty expected_ty
- ; return $ coiToHsWrapper coi
- }
- where
- outer = case sub_ctxt of -- Ugh
- SubDone -> False
- other -> True
+defer_to_boxy_matching orig act_sty actual_ty exp_ib exp_sty expected_ty
+ = do { coi <- addSubCtxt orig act_sty exp_sty $
+ u_tys (Unify True act_sty exp_sty)
+ False act_sty actual_ty exp_ib exp_sty expected_ty
+ ; return $ coiToHsWrapper coi }
-----------------------------------
-tc_sub_funs act_arg act_res exp_ib exp_arg exp_res
- = do { arg_coi <- uTys False act_arg exp_ib exp_arg
- ; co_fn_res <- tc_sub SubDone act_res act_res exp_ib exp_res exp_res
+tc_sub_funs orig act_arg act_res exp_ib exp_arg exp_res
+ = do { arg_coi <- addSubCtxt orig act_arg exp_arg $
+ uTysOuter False act_arg exp_ib exp_arg
+ ; co_fn_res <- tc_sub orig act_res act_res exp_ib exp_res exp_res
; wrapper1 <- wrapFunResCoercion [exp_arg] co_fn_res
; let wrapper2 = case arg_coi of
IdCo -> idHsWrapper
ACo co -> WpCo $ FunTy co act_res
- ; return (wrapper1 <.> wrapper2)
- }
+ ; return (wrapper1 <.> wrapper2) }
-----------------------------------
wrapFunResCoercion
= return idHsWrapper
| null arg_tys
= return co_fn_res
- | otherwise
+ | otherwise
= do { arg_ids <- newSysLocalIds FSLIT("sub") arg_tys
; return (mkWpLams arg_ids <.> co_fn_res <.> mkWpApps arg_ids) }
\end{code}
; let skol_info = GenSkol forall_tvs (mkPhiTy theta rho_ty)
; return ((forall_tvs, theta, rho_ty), skol_info) })
-#ifdef DEBUG
- ; traceTc (text "tcGen" <+> vcat [text "extra_tvs" <+> ppr extra_tvs,
- text "expected_ty" <+> ppr expected_ty,
- text "inst ty" <+> ppr tvs' <+> ppr theta' <+> ppr rho',
- text "free_tvs" <+> ppr free_tvs])
-#endif
+ ; when debugIsOn $
+ traceTc (text "tcGen" <+> vcat [
+ text "extra_tvs" <+> ppr extra_tvs,
+ text "expected_ty" <+> ppr expected_ty,
+ text "inst ty" <+> ppr tvs' <+> ppr theta'
+ <+> ppr rho',
+ text "free_tvs" <+> ppr free_tvs])
-- Type-check the arg and unify with poly type
; (result, lie) <- getLIE (thing_inside tvs' rho')
-- list of "free vars" for the signature check.
; loc <- getInstLoc (SigOrigin skol_info)
- ; dicts <- newDictBndrs loc theta'
+ ; dicts <- newDictBndrs loc theta' -- Includes equalities
; inst_binds <- tcSimplifyCheck loc tvs' dicts lie
; checkSigTyVarsWrt free_tvs tvs'
-- The WpLet binds any Insts which came out of the simplification.
dict_vars = map instToVar dicts
co_fn = mkWpTyLams tvs' <.> mkWpLams dict_vars <.> WpLet inst_binds
- ; returnM (co_fn, result) }
+ ; return (co_fn, result) }
where
free_tvs = tyVarsOfType expected_ty `unionVarSet` extra_tvs
\end{code}
\begin{code}
boxyUnify :: BoxyType -> BoxyType -> TcM CoercionI
-- Acutal and expected, respectively
-boxyUnify ty1 ty2
- = addErrCtxtM (unifyCtxt ty1 ty2) $
- uTysOuter False ty1 False ty2
+boxyUnify ty1 ty2 = addErrCtxtM (unifyCtxt ty1 ty2) $
+ uTysOuter False ty1 False ty2
---------------
boxyUnifyList :: [BoxyType] -> [BoxyType] -> TcM [CoercionI]
---------------
unifyPred :: PredType -> PredType -> TcM CoercionI
-- Acutal and expected types
-unifyPred p1 p2 = addErrCtxtM (unifyCtxt (mkPredTy p1) (mkPredTy p2)) $
- uPred True True p1 True p2
+unifyPred p1 p2 = uPred (Unify False (mkPredTy p1) (mkPredTy p2)) True p1 True p2
unifyTheta :: TcThetaType -> TcThetaType -> TcM [CoercionI]
-- Acutal and expected types
\begin{code}
unifyTypeList :: [TcTauType] -> TcM ()
-unifyTypeList [] = returnM ()
-unifyTypeList [ty] = returnM ()
+unifyTypeList [] = return ()
+unifyTypeList [ty] = return ()
unifyTypeList (ty1:tys@(ty2:_)) = do { unifyType ty1 ty2
; unifyTypeList tys }
\end{code}
-- we must not allow polytypes. But if we are in a box on
-- just one side, then we can allow polytypes
-type Outer = Bool -- True <=> this is the outer level of a unification
- -- so that the types being unified are the
- -- very ones we began with, not some sub
- -- component or synonym expansion
--- The idea is that if Outer is true then unifyMisMatch should
--- pop the context to remove the "Expected/Acutal" context
+data Outer = Unify Bool TcType TcType
+ -- If there is a unification error, report these types as mis-matching
+ -- Bool = True <=> the context says "Expected = ty1, Acutal = ty2"
+ -- for this particular ty1,ty2
-uTysOuter, uTys
- :: InBox -> TcType -- ty1 is the *actual* type
- -> InBox -> TcType -- ty2 is the *expected* type
- -> TcM CoercionI
+instance Outputable Outer where
+ ppr (Unify c ty1 ty2) = pp_c <+> pprParendType ty1 <+> ptext SLIT("~")
+ <+> pprParendType ty2
+ where
+ pp_c = if c then ptext SLIT("Top") else ptext SLIT("NonTop")
+
+
+-------------------------
+uTysOuter :: InBox -> TcType -- ty1 is the *actual* type
+ -> InBox -> TcType -- ty2 is the *expected* type
+ -> TcM CoercionI
+-- We've just pushed a context describing ty1,ty2
uTysOuter nb1 ty1 nb2 ty2
= do { traceTc (text "uTysOuter" <+> ppr ty1 <+> ppr ty2)
- ; u_tys True nb1 ty1 ty1 nb2 ty2 ty2 }
+ ; u_tys (Unify True ty1 ty2) nb1 ty1 ty1 nb2 ty2 ty2 }
+
+uTys :: InBox -> TcType -> InBox -> TcType -> TcM CoercionI
+-- The context does not describe ty1,ty2
uTys nb1 ty1 nb2 ty2
- = do { traceTc (text "uTys" <+> ppr ty1 <+> ppr ty2)
- ; u_tys False nb1 ty1 ty1 nb2 ty2 ty2 }
+ = do { traceTc (text "uTys" <+> ppr ty1 <+> ppr ty2)
+ ; u_tys (Unify False ty1 ty2) nb1 ty1 ty1 nb2 ty2 ty2 }
--------------
uTys_s :: InBox -> [TcType] -- tys1 are the *actual* types
-> InBox -> [TcType] -- tys2 are the *expected* types
-> TcM [CoercionI]
-uTys_s nb1 [] nb2 [] = returnM []
+uTys_s nb1 [] nb2 [] = return []
uTys_s nb1 (ty1:tys1) nb2 (ty2:tys2) = do { coi <- uTys nb1 ty1 nb2 ty2
; cois <- uTys_s nb1 tys1 nb2 tys2
- ; return (coi:cois)
- }
+ ; return (coi:cois) }
uTys_s nb1 ty1s nb2 ty2s = panic "Unify.uTys_s: mismatched type lists!"
--------------
-> TcM CoercionI
u_tys outer nb1 orig_ty1 ty1 nb2 orig_ty2 ty2
- = do { traceTc (text "u_tys " <+> ppr ty1 <+> text " " <+> ppr ty2)
- ; coi <- go outer ty1 ty2
+ = do { traceTc (text "u_tys " <+> vcat [sep [ braces (ppr orig_ty1 <+> text "/" <+> ppr ty1),
+ text "~",
+ braces (ppr orig_ty2 <+> text "/" <+> ppr ty2)],
+ ppr outer])
+ ; coi <- go outer orig_ty1 ty1 orig_ty2 ty2
; traceTc (case coi of
- ACo co -> text "u_tys yields coercion: " <+> ppr co
+ ACo co -> text "u_tys yields coercion:" <+> ppr co
IdCo -> text "u_tys yields no coercion")
; return coi
}
where
-
- go :: Outer -> TcType -> TcType -> TcM CoercionI
- go outer ty1 ty2 =
- do { traceTc (text "go " <+> ppr orig_ty1 <+> text "/" <+> ppr ty1
- <+> ppr orig_ty2 <+> text "/" <+> ppr ty2)
- ; go1 outer ty1 ty2
- }
-
- go1 :: Outer -> TcType -> TcType -> TcM CoercionI
+ bale_out :: Outer -> TcM a
+ bale_out outer = unifyMisMatch outer
+ -- We report a mis-match in terms of the original arugments to
+ -- u_tys, even though 'go' has recursed inwards somewhat
+ --
+ -- Note [Unifying AppTy]
+ -- A case in point is unifying (m Int) ~ (IO Int)
+ -- where m is a unification variable that is now bound to (say) (Bool ->)
+ -- Then we want to report "Can't unify (Bool -> Int) with (IO Int)
+ -- and not "Can't unify ((->) Bool) with IO"
+
+ go :: Outer -> TcType -> TcType -> TcType -> TcType -> TcM CoercionI
-- Always expand synonyms: see Note [Unification and synonyms]
-- (this also throws away FTVs)
- go1 outer ty1 ty2
- | Just ty1' <- tcView ty1 = go False ty1' ty2
- | Just ty2' <- tcView ty2 = go False ty1 ty2'
+ go outer sty1 ty1 sty2 ty2
+ | Just ty1' <- tcView ty1 = go (Unify False ty1' ty2 ) sty1 ty1' sty2 ty2
+ | Just ty2' <- tcView ty2 = go (Unify False ty1 ty2') sty1 ty1 sty2 ty2'
-- Variables; go for uVar
- go1 outer (TyVarTy tyvar1) ty2 = uVar outer False tyvar1 nb2 orig_ty2 ty2
- go1 outer ty1 (TyVarTy tyvar2) = uVar outer True tyvar2 nb1 orig_ty1 ty1
+ go outer sty1 (TyVarTy tyvar1) sty2 ty2 = uVar outer False tyvar1 nb2 sty2 ty2
+ go outer sty1 ty1 sty2 (TyVarTy tyvar2) = uVar outer True tyvar2 nb1 sty1 ty1
-- "True" means args swapped
-- The case for sigma-types must *follow* the variable cases
-- because a boxy variable can be filed with a polytype;
-- but must precede FunTy, because ((?x::Int) => ty) look
-- like a FunTy; there isn't necy a forall at the top
- go1 _ ty1 ty2
+ go _ _ ty1 _ ty2
| isSigmaTy ty1 || isSigmaTy ty2
= do { traceTc (text "We have sigma types: equalLength" <+> ppr tvs1 <+> ppr tvs2)
- ; checkM (equalLength tvs1 tvs2)
- (unifyMisMatch outer False orig_ty1 orig_ty2)
+ ; unless (equalLength tvs1 tvs2) (bale_out outer)
; traceTc (text "We're past the first length test")
; tvs <- tcInstSkolTyVars UnkSkol tvs1 -- Not a helpful SkolemInfo
-- Get location from monad, not from tvs1
(theta2,tau2) = tcSplitPhiTy phi2
; addErrCtxtM (unifyForAllCtxt tvs phi1 phi2) $ do
- { checkM (equalLength theta1 theta2)
- (unifyMisMatch outer False orig_ty1 orig_ty2)
-
- ; cois <- uPreds False nb1 theta1 nb2 theta2 -- TOMDO: do something with these pred_cois
+ { unless (equalLength theta1 theta2) (bale_out outer)
+ ; cois <- uPreds outer nb1 theta1 nb2 theta2 -- TOMDO: do something with these pred_cois
; traceTc (text "TOMDO!")
; coi <- uTys nb1 tau1 nb2 tau2
-- Check for escape; e.g. (forall a. a->b) ~ (forall a. a->a)
; free_tvs <- zonkTcTyVarsAndFV (varSetElems (tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2))
- ; ifM (any (`elemVarSet` free_tvs) tvs)
+ ; when (any (`elemVarSet` free_tvs) tvs)
(bleatEscapedTvs free_tvs tvs tvs)
-- If both sides are inside a box, we are in a "box-meets-box"
-- the same polytype... but it should be a monotype.
-- This check comes last, because the error message is
-- extremely unhelpful.
- ; ifM (nb1 && nb2) (notMonoType ty1)
+ ; when (nb1 && nb2) (notMonoType ty1)
; return coi
}}
where
(tvs2, body2) = tcSplitForAllTys ty2
-- Predicates
- go1 outer (PredTy p1) (PredTy p2)
- = uPred False nb1 p1 nb2 p2
+ go outer _ (PredTy p1) _ (PredTy p2)
+ = uPred outer nb1 p1 nb2 p2
-- Type constructors must match
- go1 _ (TyConApp con1 tys1) (TyConApp con2 tys2)
+ go _ _ (TyConApp con1 tys1) _ (TyConApp con2 tys2)
| con1 == con2 && not (isOpenSynTyCon con1)
= do { cois <- uTys_s nb1 tys1 nb2 tys2
; return $ mkTyConAppCoI con1 tys1 cois
-- See Note [OpenSynTyCon app]
-- Functions; just check the two parts
- go1 _ (FunTy fun1 arg1) (FunTy fun2 arg2)
+ go _ _ (FunTy fun1 arg1) _ (FunTy fun2 arg2)
= do { coi_l <- uTys nb1 fun1 nb2 fun2
; coi_r <- uTys nb1 arg1 nb2 arg2
; return $ mkFunTyCoI fun1 coi_l arg1 coi_r
-- They can match FunTy and TyConApp, so use splitAppTy_maybe
-- NB: we've already dealt with type variables and Notes,
-- so if one type is an App the other one jolly well better be too
- go1 outer (AppTy s1 t1) ty2
+ go outer _ (AppTy s1 t1) _ ty2
| Just (s2,t2) <- tcSplitAppTy_maybe ty2
- = do { coi_s <- uTys nb1 s1 nb2 s2; coi_t <- uTys nb1 t1 nb2 t2
+ = do { coi_s <- go outer s1 s1 s2 s2 -- NB recurse into go
+ ; coi_t <- uTys nb1 t1 nb2 t2 -- See Note [Unifying AppTy]
; return $ mkAppTyCoI s1 coi_s t1 coi_t }
-- Now the same, but the other way round
-- Don't swap the types, because the error messages get worse
- go1 outer ty1 (AppTy s2 t2)
+ go outer _ ty1 _ (AppTy s2 t2)
| Just (s1,t1) <- tcSplitAppTy_maybe ty1
- = do { coi_s <- uTys nb1 s1 nb2 s2; coi_t <- uTys nb1 t1 nb2 t2
+ = do { coi_s <- go outer s1 s1 s2 s2
+ ; coi_t <- uTys nb1 t1 nb2 t2
; return $ mkAppTyCoI s1 coi_s t1 coi_t }
-- One or both outermost constructors are type family applications.
-- If we can normalise them away, proceed as usual; otherwise, we
-- need to defer unification by generating a wanted equality constraint.
- go1 outer ty1 ty2
+ go outer sty1 ty1 sty2 ty2
| ty1_is_fun || ty2_is_fun
= do { (coi1, ty1') <- if ty1_is_fun then tcNormaliseFamInst ty1
else return (IdCo, ty1)
defer_unification outer False orig_ty1 orig_ty2
}
else -- unification can proceed
- go outer ty1' ty2'
+ go outer sty1 ty1' sty2 ty2'
; return $ coi1 `mkTransCoI` coi `mkTransCoI` (mkSymCoI coi2)
}
where
ty2_is_fun = isOpenSynTyConApp ty2
-- Anything else fails
- go1 outer _ _ = unifyMisMatch outer False orig_ty1 orig_ty2
-
+ go outer _ _ _ _ = bale_out outer
----------
uPred outer nb1 (IParam n1 t1) nb2 (IParam n2 t2)
do { cois <- uTys_s nb1 tys1 nb2 tys2 -- Guaranteed equal lengths because the kinds check
; return $ mkClassPPredCoI c1 tys1 cois
}
-uPred outer _ p1 _ p2 = unifyMisMatch outer False (mkPredTy p1) (mkPredTy p2)
+uPred outer _ p1 _ p2 = unifyMisMatch outer
uPreds outer nb1 [] nb2 [] = return []
uPreds outer nb1 (p1:ps1) nb2 (p2:ps2) =
- do { coi <- uPred outer nb1 p1 nb2 p2
+ do { coi <- uPred outer nb1 p1 nb2 p2
; cois <- uPreds outer nb1 ps1 nb2 ps2
; return (coi:cois)
}
-uPreds outer nb1 ps1 nb2 ps2 = panic "uPreds"
+uPreds outer nb1 ps1 nb2 ps2 = panic "uPreds"
\end{code}
Note [TyCon app]
uVar outer swapped tv1 nb2 ps_ty2 ty2
= do { let expansion | showSDoc (ppr ty2) == showSDoc (ppr ps_ty2) = empty
| otherwise = brackets (equals <+> ppr ty2)
- ; traceTc (text "uVar" <+> ppr swapped <+>
+ ; traceTc (text "uVar" <+> ppr outer <+> ppr swapped <+>
sep [ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1 ),
nest 2 (ptext SLIT(" <-> ")),
ppr ps_ty2 <+> dcolon <+> ppr (typeKind ty2) <+> expansion])
uUnfilledVar outer swapped tv1 details1 ps_ty2 ty2
| Just ty2' <- tcView ty2
= -- Expand synonyms; ignore FTVs
- uUnfilledVar False swapped tv1 details1 ps_ty2 ty2'
+ let outer' | swapped = Unify False ty2' (mkTyVarTy tv1)
+ | otherwise = Unify False (mkTyVarTy tv1) ty2'
+ in uUnfilledVar outer' swapped tv1 details1 ps_ty2 ty2'
uUnfilledVar outer swapped tv1 details1 ps_ty2 (TyVarTy tv2)
| tv1 == tv2 -- Same type variable => no-op (but watch out for the boxy case)
; updateMeta tv1 ref1 (mkTyVarTy tau_tv)
; return IdCo
}
- other -> returnM IdCo -- No-op
+ other -> return IdCo -- No-op
| otherwise -- Distinct type variables
= do { lookup2 <- lookupTcTyVar tv2
= -- ty2 is not a type variable
case details1 of
MetaTv (SigTv _) _ -> rigid_variable
- MetaTv info ref1 ->
- uMetaVar outer swapped tv1 info ref1 ps_ty2 non_var_ty2
+ MetaTv info ref1 -> uMetaVar outer swapped tv1 info ref1 ps_ty2 non_var_ty2
SkolemTv _ -> rigid_variable
where
rigid_variable
}
| SkolemTv RuntimeUnkSkol <- details1
-- runtime unknown will never match
- = unifyMisMatch outer swapped (TyVarTy tv1) ps_ty2
+ = unifyMisMatch outer
| otherwise -- defer as a given equality may still resolve this
= defer_unification outer swapped (TyVarTy tv1) ps_ty2
\end{code}
to zonk in zonInst instead. Would that be sufficient?)
\begin{code}
-defer_unification :: Bool -- pop innermost context?
+defer_unification :: Outer
-> SwapFlag
-> TcType
-> TcType
; cotv <- newMetaCoVar ty1' ty2'
-- put ty1 ~ ty2 in LIE
-- Left means "wanted"
- ; inst <- (if outer then popErrCtxt else id) $
+ ; inst <- popUnifyCtxt outer $
mkEqInst (EqPred ty1' ty2') (Left cotv)
; extendLIE inst
; return $ ACo $ TyVarTy cotv }
----------------
-uMetaVar :: Bool -- pop innermost context?
+uMetaVar :: Outer
-> SwapFlag
-> TcTyVar -> BoxInfo -> IORef MetaDetails
-> TcType -> TcType
--
-- It should not be the case that tv1 occurs in ty2
-- (i.e. no occurs check should be needed), but if perchance
- -- it does, the unbox operation will fill it, and the DEBUG
+ -- it does, the unbox operation will fill it, and the debug code
-- checks for that.
- do { final_ty <- unBox ps_ty2
-#ifdef DEBUG
- ; meta_details <- readMutVar ref1
- ; case meta_details of
- Indirect ty -> WARN( True, ppr tv1 <+> ppr ty )
- return () -- This really should *not* happen
- Flexi -> return ()
-#endif
- ; checkUpdateMeta swapped tv1 ref1 final_ty
+ do { final_ty <- unBox ps_ty2
+ ; when debugIsOn $ do
+ { meta_details <- readMutVar ref1
+ ; case meta_details of
+ Indirect ty -> WARN( True, ppr tv1 <+> ppr ty )
+ return () -- This really should *not* happen
+ Flexi -> return ()
+ }
+ ; checkUpdateMeta swapped tv1 ref1 final_ty
; return IdCo
}
--
-- For once, it's safe to treat synonyms as opaque!
-unBox (NoteTy n ty) = do { ty' <- unBox ty; return (NoteTy n ty') }
unBox (TyConApp tc tys) = do { tys' <- mapM unBox tys; return (TyConApp tc tys') }
unBox (AppTy f a) = do { f' <- unBox f; a' <- unBox a; return (mkAppTy f' a') }
unBox (FunTy f a) = do { f' <- unBox f; a' <- unBox a; return (FunTy f' a') }
%************************************************************************
%* *
-\subsection[Unify-context]{Errors and contexts}
+ Errors and contexts
%* *
%************************************************************************
-Errors
-~~~~~~
-
\begin{code}
+unifyMisMatch :: Outer -> TcM a
+unifyMisMatch (Unify is_outer ty1 ty2)
+ | is_outer = popErrCtxt $ failWithMisMatch ty1 ty2 -- This is the whole point of the 'outer' stuff
+ | otherwise = failWithMisMatch ty1 ty2
+
+popUnifyCtxt :: Outer -> TcM a -> TcM a
+popUnifyCtxt (Unify True _ _) thing = popErrCtxt thing
+popUnifyCtxt (Unify False _ _) thing = thing
+
+-----------------------
unifyCtxt act_ty exp_ty tidy_env
= do { act_ty' <- zonkTcType act_ty
; exp_ty' <- zonkTcType exp_ty
----------------
-- If an error happens we try to figure out whether the function
-- function has been given too many or too few arguments, and say so.
-addSubCtxt SubDone actual_res_ty expected_res_ty thing_inside
- = thing_inside
-addSubCtxt sub_ctxt actual_res_ty expected_res_ty thing_inside
+addSubCtxt orig actual_res_ty expected_res_ty thing_inside
= addErrCtxtM mk_err thing_inside
where
mk_err tidy_env
len_act_args = length act_args
len_exp_args = length exp_args
- message = case sub_ctxt of
- SubFun fun | len_exp_args < len_act_args -> wrongArgsCtxt "too few" fun
- | len_exp_args > len_act_args -> wrongArgsCtxt "too many" fun
- other -> mkExpectedActualMsg act_ty'' exp_ty''
+ message = case orig of
+ OccurrenceOf fun
+ | len_exp_args < len_act_args -> wrongArgsCtxt "too few" fun
+ | len_exp_args > len_act_args -> wrongArgsCtxt "too many" fun
+ other -> mkExpectedActualMsg act_ty'' exp_ty''
; return (env2, message) }
wrongArgsCtxt too_many_or_few fun
------------------
unifyForAllCtxt tvs phi1 phi2 env
- = returnM (env2, msg)
+ = return (env2, msg)
where
(env', tvs') = tidyOpenTyVars env tvs -- NB: not tidyTyVarBndrs
(env1, phi1') = tidyOpenType env' phi1
(env2, phi2') = tidyOpenType env1 phi2
msg = vcat [ptext SLIT("When matching") <+> quotes (ppr (mkForAllTys tvs' phi1')),
ptext SLIT(" and") <+> quotes (ppr (mkForAllTys tvs' phi2'))]
-
------------------------
-unifyMisMatch outer swapped ty1 ty2
- | swapped = unifyMisMatch outer False ty2 ty1
- | outer = popErrCtxt $ unifyMisMatch False swapped ty1 ty2 -- This is the whole point of the 'outer' stuff
- | otherwise = failWithMisMatch ty1 ty2
\end{code}
+
%************************************************************************
%* *
Kind unification
-> TcKind -- Actual
-> TcM ()
unifyKind (TyConApp kc1 []) (TyConApp kc2 [])
- | isSubKindCon kc2 kc1 = returnM ()
+ | isSubKindCon kc2 kc1 = return ()
unifyKind (FunTy a1 r1) (FunTy a2 r2)
= do { unifyKind a2 a1; unifyKind r1 r2 }
unifyKind k1 k2 = unifyKindMisMatch k1 k2
unifyKinds :: [TcKind] -> [TcKind] -> TcM ()
-unifyKinds [] [] = returnM ()
-unifyKinds (k1:ks1) (k2:ks2) = unifyKind k1 k2 `thenM_`
- unifyKinds ks1 ks2
-unifyKinds _ _ = panic "unifyKinds: length mis-match"
+unifyKinds [] [] = return ()
+unifyKinds (k1:ks1) (k2:ks2) = do unifyKind k1 k2
+ unifyKinds ks1 ks2
+unifyKinds _ _ = panic "unifyKinds: length mis-match"
----------------
uKVar :: Bool -> KindVar -> TcKind -> TcM ()
----------------
uUnboundKVar :: Bool -> KindVar -> TcKind -> TcM ()
uUnboundKVar swapped kv1 k2@(TyVarTy kv2)
- | kv1 == kv2 = returnM ()
+ | kv1 == kv2 = return ()
| otherwise -- Distinct kind variables
= do { mb_k2 <- readKindVar kv2
; case mb_k2 of
unifyFunKind :: TcKind -> TcM (Maybe (TcKind, TcKind))
-- Like unifyFunTy, but does not fail; instead just returns Nothing
-unifyFunKind (TyVarTy kvar)
- = readKindVar kvar `thenM` \ maybe_kind ->
+unifyFunKind (TyVarTy kvar) = do
+ maybe_kind <- readKindVar kvar
case maybe_kind of
Indirect fun_kind -> unifyFunKind fun_kind
Flexi ->
do { arg_kind <- newKindVar
; res_kind <- newKindVar
; writeKindVar kvar (mkArrowKind arg_kind res_kind)
- ; returnM (Just (arg_kind,res_kind)) }
+ ; return (Just (arg_kind,res_kind)) }
-unifyFunKind (FunTy arg_kind res_kind) = returnM (Just (arg_kind,res_kind))
-unifyFunKind other = returnM Nothing
+unifyFunKind (FunTy arg_kind res_kind) = return (Just (arg_kind,res_kind))
+unifyFunKind other = return Nothing
\end{code}
%************************************************************************
-- The first argument, ty, is used only in the error message generation
checkExpectedKind ty act_kind exp_kind
| act_kind `isSubKind` exp_kind -- Short cut for a very common case
- = returnM ()
- | otherwise
- = tryTc (unifyKind exp_kind act_kind) `thenM` \ (_errs, mb_r) ->
- case mb_r of {
- Just r -> returnM () ; -- Unification succeeded
- Nothing ->
+ = return ()
+ | otherwise = do
+ (_errs, mb_r) <- tryTc (unifyKind exp_kind act_kind)
+ case mb_r of
+ Just r -> return () ; -- Unification succeeded
+ Nothing -> do
-- So there's definitely an error
-- Now to find out what sort
- zonkTcKind exp_kind `thenM` \ exp_kind ->
- zonkTcKind act_kind `thenM` \ act_kind ->
-
- tcInitTidyEnv `thenM` \ env0 ->
- let (exp_as, _) = splitKindFunTys exp_kind
- (act_as, _) = splitKindFunTys act_kind
- n_exp_as = length exp_as
- n_act_as = length act_as
-
- (env1, tidy_exp_kind) = tidyKind env0 exp_kind
- (env2, tidy_act_kind) = tidyKind env1 act_kind
-
- err | n_exp_as < n_act_as -- E.g. [Maybe]
- = quotes (ppr ty) <+> ptext SLIT("is not applied to enough type arguments")
-
- -- Now n_exp_as >= n_act_as. In the next two cases,
- -- n_exp_as == 0, and hence so is n_act_as
- | isLiftedTypeKind exp_kind && isUnliftedTypeKind act_kind
- = ptext SLIT("Expecting a lifted type, but") <+> quotes (ppr ty)
- <+> ptext SLIT("is unlifted")
-
- | isUnliftedTypeKind exp_kind && isLiftedTypeKind act_kind
- = ptext SLIT("Expecting an unlifted type, but") <+> quotes (ppr ty)
- <+> ptext SLIT("is lifted")
-
- | otherwise -- E.g. Monad [Int]
- = ptext SLIT("Kind mis-match")
-
- more_info = sep [ ptext SLIT("Expected kind") <+>
- quotes (pprKind tidy_exp_kind) <> comma,
- ptext SLIT("but") <+> quotes (ppr ty) <+>
- ptext SLIT("has kind") <+> quotes (pprKind tidy_act_kind)]
- in
- failWithTcM (env2, err $$ more_info)
- }
+ exp_kind <- zonkTcKind exp_kind
+ act_kind <- zonkTcKind act_kind
+
+ env0 <- tcInitTidyEnv
+ let (exp_as, _) = splitKindFunTys exp_kind
+ (act_as, _) = splitKindFunTys act_kind
+ n_exp_as = length exp_as
+ n_act_as = length act_as
+
+ (env1, tidy_exp_kind) = tidyKind env0 exp_kind
+ (env2, tidy_act_kind) = tidyKind env1 act_kind
+
+ err | n_exp_as < n_act_as -- E.g. [Maybe]
+ = quotes (ppr ty) <+> ptext SLIT("is not applied to enough type arguments")
+
+ -- Now n_exp_as >= n_act_as. In the next two cases,
+ -- n_exp_as == 0, and hence so is n_act_as
+ | isLiftedTypeKind exp_kind && isUnliftedTypeKind act_kind
+ = ptext SLIT("Expecting a lifted type, but") <+> quotes (ppr ty)
+ <+> ptext SLIT("is unlifted")
+
+ | isUnliftedTypeKind exp_kind && isLiftedTypeKind act_kind
+ = ptext SLIT("Expecting an unlifted type, but") <+> quotes (ppr ty)
+ <+> ptext SLIT("is lifted")
+
+ | otherwise -- E.g. Monad [Int]
+ = ptext SLIT("Kind mis-match")
+
+ more_info = sep [ ptext SLIT("Expected kind") <+>
+ quotes (pprKind tidy_exp_kind) <> comma,
+ ptext SLIT("but") <+> quotes (ppr ty) <+>
+ ptext SLIT("has kind") <+> quotes (pprKind tidy_act_kind)]
+
+ failWithTcM (env2, err $$ more_info)
\end{code}
%************************************************************************
-- Guaranteed to be skolems
-> TcM ()
check_sig_tyvars extra_tvs []
- = returnM ()
+ = return ()
check_sig_tyvars extra_tvs sig_tvs
= ASSERT( all isSkolemTyVar sig_tvs )
do { gbl_tvs <- tcGetGlobalTyVars
text "extra_tvs" <+> ppr extra_tvs]))
; let env_tvs = gbl_tvs `unionVarSet` extra_tvs
- ; ifM (any (`elemVarSet` env_tvs) sig_tvs)
- (bleatEscapedTvs env_tvs sig_tvs sig_tvs)
+ ; when (any (`elemVarSet` env_tvs) sig_tvs)
+ (bleatEscapedTvs env_tvs sig_tvs sig_tvs)
}
bleatEscapedTvs :: TcTyVarSet -- The global tvs
| not (zonked_tv `elemVarSet` globals) = return (tidy_env, msgs)
| otherwise
= do { (tidy_env1, globs) <- findGlobals (unitVarSet zonked_tv) tidy_env
- ; returnM (tidy_env1, escape_msg sig_tv zonked_tv globs : msgs) }
+ ; return (tidy_env1, escape_msg sig_tv zonked_tv globs : msgs) }
-----------------------
escape_msg sig_tv zonked_tv globs
\begin{code}
sigCtxt :: Id -> [TcTyVar] -> TcThetaType -> TcTauType
-> TidyEnv -> TcM (TidyEnv, Message)
-sigCtxt id sig_tvs sig_theta sig_tau tidy_env
- = zonkTcType sig_tau `thenM` \ actual_tau ->
+sigCtxt id sig_tvs sig_theta sig_tau tidy_env = do
+ actual_tau <- zonkTcType sig_tau
let
(env1, tidy_sig_tvs) = tidyOpenTyVars tidy_env sig_tvs
(env2, tidy_sig_rho) = tidyOpenType env1 (mkPhiTy sig_theta sig_tau)
]
msg = vcat [ptext SLIT("When trying to generalise the type inferred for") <+> quotes (ppr id),
nest 2 sub_msg]
- in
- returnM (env3, msg)
+
+ return (env3, msg)
\end{code}
projects / ghc-hetmet.git / blobdiff