Type subsumption and unification
\begin{code}
-{-# OPTIONS -w #-}
--- The above warning supression flag is a temporary kludge.
--- While working on this module you are encouraged to remove it and fix
--- any warnings in the module. See
--- http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings
--- for details
-
module TcUnify (
-- Full-blown subsumption
tcSubExp, tcGen,
-- Various unifications
unifyType, unifyTypeList, unifyTheta,
unifyKind, unifyKinds, unifyFunKind,
- checkExpectedKind,
preSubType, boxyMatchTypes,
--------------------------------
import BasicTypes
import Util
import Outputable
-import Unique
import FastString
import Control.Monad
subFunTys :: SDoc -- Something like "The function f has 3 arguments"
-- or "The abstraction (\x.e) takes 1 argument"
-> Arity -- Expected # of args
- -> BoxyRhoType -- res_ty
+ -> BoxySigmaType -- res_ty
+ -> Maybe UserTypeCtxt -- Whether res_ty arises from a user signature
+ -- Only relevant if we encounter a sigma-type
-> ([BoxySigmaType] -> BoxyRhoType -> TcM a)
-> TcM (HsWrapper, a)
-- Attempt to decompse res_ty to have enough top-level arrows to
-}
-subFunTys error_herald n_pats res_ty thing_inside
+subFunTys error_herald n_pats res_ty mb_ctxt thing_inside
= loop n_pats [] res_ty
where
-- In 'loop', the parameter 'arg_tys' accumulates
| isSigmaTy res_ty -- Do this before checking n==0, because we
-- guarantee to return a BoxyRhoType, not a
-- BoxySigmaType
- = do { (gen_fn, (co_fn, res)) <- tcGen res_ty emptyVarSet $ \ _ res_ty' ->
- loop n args_so_far res_ty'
+ = do { (gen_fn, (co_fn, res)) <- tcGen res_ty emptyVarSet mb_ctxt $ \ _ res_ty ->
+ loop n args_so_far res_ty
; return (gen_fn <.> co_fn, res) }
loop 0 args_so_far res_ty
; return (co_fn', res) }
-- Try to normalise synonym families and defer if that's not possible
- loop n args_so_far ty@(TyConApp tc tys)
+ loop n args_so_far ty@(TyConApp tc _)
| isOpenSynTyCon tc
= do { (coi1, ty') <- tcNormaliseFamInst ty
; case coi1 of
-- Note argTypeKind: the args can have an unboxed type,
-- but not an unboxed tuple.
- loop n args_so_far res_ty = bale_out args_so_far
+ loop _ args_so_far _ = bale_out args_so_far
-- Build a template type a1 -> ... -> an -> b and defer an equality
-- between that template and the expected result type res_ty; then,
= do { (coi1, ty') <- tcNormaliseFamInst ty
; case coi1 of
IdCo -> defer -- no progress, but maybe solvable => defer
- ACo co -> -- progress: so lets try again
+ ACo _ -> -- progress: so lets try again
do { (args, coi2) <- loop ty'
; return $ (args, coi2 `mkTransCoI` mkSymCoI coi1)
}
mk_res_ty _other = panic "TcUnify.mk_res_ty2"
------------------
+boxySplitFailure :: TcType -> TcType -> TcM (a, CoercionI)
boxySplitFailure actual_ty expected_ty = failWithMisMatch actual_ty expected_ty
------------------
| Just t_ty' <- tcView t_ty = go t_tvs t_ty' b_tvs b_ty
| Just b_ty' <- tcView b_ty = go t_tvs t_ty b_tvs b_ty'
- go t_tvs (TyVarTy _) b_tvs b_ty = emptyTvSubst -- Rule S-ANY; no bindings
+ go _ (TyVarTy _) _ _ = emptyTvSubst -- Rule S-ANY; no bindings
-- Rule S-ANY covers (a) type variables and (b) boxy types
-- in the template. Both look like a TyVarTy.
-- See Note [Sub-match] below
boxy_match_s tmpl_tvs tmpl_tys emptyVarSet boxy_tys emptyTvSubst
-- ToDo: add error context?
-boxy_match_s tmpl_tvs [] boxy_tvs [] subst
+boxy_match_s :: TcTyVarSet -> [TcType] -> TcTyVarSet -> [BoxySigmaType]
+ -> TvSubst -> TvSubst
+boxy_match_s _ [] _ [] subst
= subst
boxy_match_s tmpl_tvs (t_ty:t_tys) boxy_tvs (b_ty:b_tys) subst
= boxy_match tmpl_tvs t_ty boxy_tvs b_ty $
boxy_match_s tmpl_tvs t_tys boxy_tvs b_tys subst
-boxy_match_s tmpl_tvs _ boxy_tvs _ subst
+boxy_match_s _ _ _ _ _
= panic "boxy_match_s" -- Lengths do not match
Nothing -> orig_boxy_ty
Just ty -> ty `boxyLub` orig_boxy_ty
- go _ (TyVarTy tv) | isMetaTyVar tv
+ go _ (TyVarTy tv) | isTcTyVar tv && isMetaTyVar tv
+ -- NB: A TyVar (not TcTyVar) is possible here, representing
+ -- a skolem, because in this pure boxy_match function
+ -- we don't instantiate foralls to TcTyVars; cf Trac #2714
= 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
| tc1 == tc2, length ts1 == length ts2
= TyConApp tc1 (zipWith boxyLub ts1 ts2)
- go (TyVarTy tv1) ty2 -- This is the whole point;
+ go (TyVarTy tv1) _ -- This is the whole point;
| isTcTyVar tv1, isBoxyTyVar tv1 -- choose ty2 if ty2 is a box
= orig_ty2
- go ty1 (TyVarTy tv2) -- Symmetrical case
+ go _ (TyVarTy tv2) -- Symmetrical case
| isTcTyVar tv2, isBoxyTyVar tv2
= orig_ty1
| Just ty2' <- tcView ty1 = go ty1 ty2'
-- For now, we don't look inside ForAlls, PredTys
- go ty1 ty2 = orig_ty1 -- Default
+ go _ _ = orig_ty1 -- Default
\end{code}
Note [Matching kinds]
-- This indirection is just here to make
-- it easy to insert a debug trace!
+tc_sub1 :: InstOrigin -> BoxySigmaType -> BoxySigmaType -> InBox
+ -> BoxySigmaType -> Type -> TcM HsWrapper
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
if exp_ib then -- SKOL does not apply if exp_ty is inside a box
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 ->
+ { (gen_fn, co_fn) <- tcGen exp_ty act_tvs Nothing $ \ _ body_exp_ty ->
tc_sub orig act_sty act_ty False body_exp_ty body_exp_ty
; return (gen_fn <.> co_fn) }
}
-- expected_ty: Int -> Int
-- co_fn e = e Int dOrdInt
-tc_sub1 orig act_sty actual_ty exp_ib exp_sty expected_ty
+tc_sub1 orig _ 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.)
-----------------------------------
-- Function case (rule F1)
-tc_sub1 orig act_sty (FunTy act_arg act_res) exp_ib exp_sty (FunTy exp_arg exp_res)
+tc_sub1 orig _ (FunTy act_arg act_res) exp_ib _ (FunTy exp_arg exp_res)
= do { traceTc (text "tc_sub1 - case 4")
; tc_sub_funs orig act_arg act_res exp_ib exp_arg exp_res
}
; 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"
+ mk_res_ty _ = panic "TcUnify.mk_res_ty3"
fun_kinds = [argTypeKind, openTypeKind]
-- Everything else: defer to boxy matching
}
-----------------------------------
+defer_to_boxy_matching :: InstOrigin -> TcType -> TcType -> InBox
+ -> TcType -> TcType -> TcM HsWrapper
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)
; return $ coiToHsWrapper coi }
-----------------------------------
+tc_sub_funs :: InstOrigin -> TcType -> BoxySigmaType -> InBox
+ -> TcType -> BoxySigmaType -> TcM HsWrapper
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
%************************************************************************
\begin{code}
-tcGen :: BoxySigmaType -- expected_ty
- -> TcTyVarSet -- Extra tyvars that the universally
- -- quantified tyvars of expected_ty
- -- must not be unified
+tcGen :: BoxySigmaType -- expected_ty
+ -> TcTyVarSet -- Extra tyvars that the universally
+ -- quantified tyvars of expected_ty
+ -- must not be unified
+ -> Maybe UserTypeCtxt -- Just ctxt => this polytype arose directly
+ -- from a user type sig
+ -- Nothing => a higher order situation
-> ([TcTyVar] -> BoxyRhoType -> TcM result)
-> TcM (HsWrapper, result)
-- The expression has type: spec_ty -> expected_ty
-tcGen expected_ty extra_tvs thing_inside -- We expect expected_ty to be a forall-type
- -- If not, the call is a no-op
+tcGen expected_ty extra_tvs mb_ctxt thing_inside -- We expect expected_ty to be a forall-type
+ -- If not, the call is a no-op
= do { traceTc (text "tcGen")
- -- We want the GenSkol info in the skolemised type variables to
- -- mention the *instantiated* tyvar names, so that we get a
- -- good error message "Rigid variable 'a' is bound by (forall a. a->a)"
- -- Hence the tiresome but innocuous fixM
- ; ((tvs', theta', rho'), skol_info) <- fixM (\ ~(_, skol_info) ->
- do { (forall_tvs, theta, rho_ty) <- tcInstSkolType skol_info expected_ty
- -- Get loation from monad, not from expected_ty
- ; let skol_info = GenSkol forall_tvs (mkPhiTy theta rho_ty)
- ; return ((forall_tvs, theta, rho_ty), skol_info) })
+ ; ((tvs', theta', rho'), skol_info) <- instantiate expected_ty
; when debugIsOn $
traceTc (text "tcGen" <+> vcat [
text "free_tvs" <+> ppr free_tvs])
-- Type-check the arg and unify with poly type
- ; (result, lie) <- getLIE (thing_inside tvs' rho')
+ ; (result, lie) <- getLIE $
+ thing_inside tvs' rho'
-- Check that the "forall_tvs" havn't been constrained
-- The interesting bit here is that we must include the free variables
; return (co_fn, result) }
where
free_tvs = tyVarsOfType expected_ty `unionVarSet` extra_tvs
+
+ instantiate :: TcType -> TcM (([TcTyVar],ThetaType,TcRhoType), SkolemInfo)
+ instantiate expected_ty
+ | Just ctxt <- mb_ctxt -- This case split is the wohle reason for mb_ctxt
+ = do { let skol_info = SigSkol ctxt
+ ; stuff <- tcInstSigType True skol_info expected_ty
+ ; return (stuff, skol_info) }
+
+ | otherwise -- We want the GenSkol info in the skolemised type variables to
+ -- mention the *instantiated* tyvar names, so that we get a
+ -- good error message "Rigid variable 'a' is bound by (forall a. a->a)"
+ -- Hence the tiresome but innocuous fixM
+ = fixM $ \ ~(_, skol_info) ->
+ do { stuff@(forall_tvs, theta, rho_ty) <- tcInstSkolType skol_info expected_ty
+ -- Get loation from *monad*, not from expected_ty
+ ; let skol_info = GenSkol forall_tvs (mkPhiTy theta rho_ty)
+ ; return (stuff, skol_info) }
\end{code}
unifyTheta theta1 theta2
= do { checkTc (equalLength theta1 theta2)
(vcat [ptext (sLit "Contexts differ in length"),
- nest 2 $ parens $ ptext (sLit "Use -fglasgow-exts to allow this")])
+ nest 2 $ parens $ ptext (sLit "Use -XRelaxedPolyRec to allow this")])
; uList unifyPred theta1 theta2
}
-- Unify corresponding elements of two lists of types, which
-- should be of equal length. We charge down the list explicitly so that
-- we can complain if their lengths differ.
-uList unify [] [] = return []
+uList _ [] [] = return []
uList unify (ty1:tys1) (ty2:tys2) = do { x <- unify ty1 ty2;
; xs <- uList unify tys1 tys2
; return (x:xs)
}
-uList unify ty1s ty2s = panic "Unify.uList: mismatched type lists!"
+uList _ _ _ = panic "Unify.uList: mismatched type lists!"
\end{code}
@unifyTypeList@ takes a single list of @TauType@s and unifies them
\begin{code}
unifyTypeList :: [TcTauType] -> TcM ()
unifyTypeList [] = return ()
-unifyTypeList [ty] = return ()
+unifyTypeList [_] = return ()
unifyTypeList (ty1:tys@(ty2:_)) = do { unifyType ty1 ty2
; unifyTypeList tys }
\end{code}
uTys_s :: InBox -> [TcType] -- tys1 are the *actual* types
-> InBox -> [TcType] -- tys2 are the *expected* types
-> TcM [CoercionI]
-uTys_s nb1 [] nb2 [] = return []
+uTys_s _ [] _ [] = 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) }
-uTys_s nb1 ty1s nb2 ty2s = panic "Unify.uTys_s: mismatched type lists!"
+uTys_s _ _ _ _ = panic "Unify.uTys_s: mismatched type lists!"
--------------
u_tys :: Outer
go :: Outer -> TcType -> TcType -> TcType -> TcType -> TcM CoercionI
-- Always expand synonyms: see Note [Unification and synonyms]
-- (this also throws away FTVs)
- go outer sty1 ty1 sty2 ty2
+ go _ 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
- 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
+ go outer _ (TyVarTy tyvar1) sty2 ty2 = uVar outer False tyvar1 nb2 sty2 ty2
+ go outer sty1 ty1 _ (TyVarTy tyvar2) = uVar outer True tyvar2 nb1 sty1 ty1
-- "True" means args swapped
-- The case for sigma-types must *follow* the variable cases
; addErrCtxtM (unifyForAllCtxt tvs phi1 phi2) $ do
{ unless (equalLength theta1 theta2) (bale_out outer)
- ; cois <- uPreds outer nb1 theta1 nb2 theta2 -- TOMDO: do something with these pred_cois
+ ; _cois <- uPreds outer nb1 theta1 nb2 theta2 -- TOMDO: do something with these pred_cois
; traceTc (text "TOMDO!")
; coi <- uTys nb1 tau1 nb2 tau2
go outer _ (PredTy p1) _ (PredTy p2)
= uPred outer nb1 p1 nb2 p2
- -- Type constructors must match
+ -- Non-synonym type constructors must match
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 [TyCon app]
+ -- Family synonyms See Note [TyCon app]
| con1 == con2 && identicalOpenSynTyConApp
= do { cois <- uTys_s nb1 tys1' nb2 tys2'
; return $ mkTyConAppCoI con1 tys1 (replicate n IdCo ++ cois)
identicalOpenSynTyConApp = idxTys1 `tcEqTypes` idxTys2
-- See Note [OpenSynTyCon app]
+ -- If we can reduce a family app => proceed with reduct
+ -- NB: We use isOpenSynTyCon, not isOpenSynTyConApp as we also must
+ -- defer oversaturated applications!
+ go outer sty1 ty1@(TyConApp con1 _) sty2 ty2
+ | isOpenSynTyCon con1
+ = do { (coi1, ty1') <- tcNormaliseFamInst ty1
+ ; case coi1 of
+ IdCo -> defer -- no reduction, see [Deferred Unification]
+ _ -> liftM (coi1 `mkTransCoI`) $ go outer sty1 ty1' sty2 ty2
+ }
+
+ -- If we can reduce a family app => proceed with reduct
+ -- NB: We use isOpenSynTyCon, not isOpenSynTyConApp as we also must
+ -- defer oversaturated applications!
+ go outer sty1 ty1 sty2 ty2@(TyConApp con2 _)
+ | isOpenSynTyCon con2
+ = do { (coi2, ty2') <- tcNormaliseFamInst ty2
+ ; case coi2 of
+ IdCo -> defer -- no reduction, see [Deferred Unification]
+ _ -> liftM (`mkTransCoI` mkSymCoI coi2) $
+ go outer sty1 ty1 sty2 ty2'
+ }
+
-- Functions; just check the two parts
go _ _ (FunTy fun1 arg1) _ (FunTy fun2 arg2)
= do { coi_l <- uTys nb1 fun1 nb2 fun2
; 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.
- 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)
- ; (coi2, ty2') <- if ty2_is_fun then tcNormaliseFamInst ty2
- else return (IdCo, ty2)
- ; coi <- if isOpenSynTyConApp ty1' || isOpenSynTyConApp ty2'
- then do { -- One type family app can't be reduced yet
- -- => defer
- ; ty1'' <- zonkTcType ty1'
- ; ty2'' <- zonkTcType ty2'
- ; if tcEqType ty1'' ty2''
- then return IdCo
- else -- see [Deferred Unification]
- defer_unification outer False orig_ty1 orig_ty2
- }
- else -- unification can proceed
- go outer sty1 ty1' sty2 ty2'
- ; return $ coi1 `mkTransCoI` coi `mkTransCoI` (mkSymCoI coi2)
- }
- where
- ty1_is_fun = isOpenSynTyConApp ty1
- ty2_is_fun = isOpenSynTyConApp ty2
-
-- Anything else fails
go outer _ _ _ _ = bale_out outer
+ defer = defer_unification outer False orig_ty1 orig_ty2
+
+
----------
-uPred outer nb1 (IParam n1 t1) nb2 (IParam n2 t2)
+uPred :: Outer -> InBox -> PredType -> InBox -> PredType -> TcM CoercionI
+uPred _ nb1 (IParam n1 t1) nb2 (IParam n2 t2)
| n1 == n2 =
do { coi <- uTys nb1 t1 nb2 t2
; return $ mkIParamPredCoI n1 coi
}
-uPred outer nb1 (ClassP c1 tys1) nb2 (ClassP c2 tys2)
+uPred _ nb1 (ClassP c1 tys1) nb2 (ClassP c2 tys2)
| c1 == c2 =
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
+uPred outer _ _ _ _ = unifyMisMatch outer
-uPreds outer nb1 [] nb2 [] = return []
+uPreds :: Outer -> InBox -> [PredType] -> InBox -> [PredType]
+ -> TcM [CoercionI]
+uPreds _ _ [] _ [] = return []
uPreds outer nb1 (p1:ps1) nb2 (p2:ps2) =
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 _ _ _ _ _ = panic "uPreds"
\end{code}
Note [TyCon app]
When we find two TyConApps, the argument lists are guaranteed equal
length. Reason: intially the kinds of the two types to be unified is
the same. The only way it can become not the same is when unifying two
-AppTys (f1 a1):=:(f2 a2). In that case there can't be a TyConApp in
-the f1,f2 (because it'd absorb the app). If we unify f1:=:f2 first,
+AppTys (f1 a1)~(f2 a2). In that case there can't be a TyConApp in
+the f1,f2 (because it'd absorb the app). If we unify f1~f2 first,
which we do, that ensures that f1,f2 have the same kind; and that
means a1,a2 have the same kind. And now the argument repeats.
-> TcM CoercionI
-- Invariant: tyvar 1 is not unified with anything
-uUnfilledVar outer swapped tv1 details1 ps_ty2 ty2
+uUnfilledVar _ swapped tv1 details1 ps_ty2 ty2
| Just ty2' <- tcView ty2
= -- Expand synonyms; ignore FTVs
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)
+uUnfilledVar outer swapped tv1 details1 _ (TyVarTy tv2)
| tv1 == tv2 -- Same type variable => no-op (but watch out for the boxy case)
= case details1 of
MetaTv BoxTv ref1 -- A boxy type variable meets itself;
; updateMeta tv1 ref1 (mkTyVarTy tau_tv)
; return IdCo
}
- other -> return IdCo -- No-op
+ _ -> return IdCo -- No-op
| otherwise -- Distinct type variables
= do { lookup2 <- lookupTcTyVar tv2
-- tv1 is an un-filled-in meta type variable (maybe boxy, maybe tau)
-- ty2 is not a type variable
-uMetaVar outer swapped tv1 BoxTv ref1 ps_ty2 non_var_ty2
+uMetaVar outer swapped tv1 BoxTv ref1 ps_ty2 ty2
= -- tv1 is a BoxTv. So we must unbox ty2, to ensure
-- that any boxes in ty2 are filled with monotypes
--
-- it does, the unbox operation will fill it, and the debug code
-- checks for that.
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
+ ; meta_details <- readMutVar ref1
+ ; case meta_details of
+ Indirect _ -> -- This *can* happen due to an occurs check,
+ -- just as it can in checkTauTvUpdate in the next
+ -- equation of uMetaVar; see Trac #2414
+ -- Note [Occurs check]
+ -- Go round again. Probably there's an immediate
+ -- error, but maybe not (a type function might discard
+ -- its argument). Next time round we'll end up in the
+ -- TauTv case of uMetaVar.
+ uVar outer swapped tv1 False ps_ty2 ty2
+ -- Setting for nb2::InBox is irrelevant
+
+ Flexi -> do { checkUpdateMeta swapped tv1 ref1 final_ty
+ ; return IdCo }
}
-uMetaVar outer swapped tv1 info1 ref1 ps_ty2 non_var_ty2
+uMetaVar outer swapped tv1 _ ref1 ps_ty2 _
= do { -- Occurs check + monotype check
; mb_final_ty <- checkTauTvUpdate tv1 ps_ty2
; case mb_final_ty of
}
}
+{- Note [Occurs check]
+ ~~~~~~~~~~~~~~~~~~~
+An eager occurs check is made in checkTauTvUpdate, deferring tricky
+cases by calling defer_unification (see notes with
+checkTauTvUpdate). An occurs check can also (and does) happen in the
+BoxTv case, but unBox doesn't check for occurrences, and in any case
+doesn't have the type-function-related complexity that
+checkTauTvUpdate has. So we content ourselves with spotting the potential
+occur check (by the fact that tv1 is now filled), and going round again.
+Next time round we'll get the TauTv case of uMetaVar.
+-}
+
----------------
uUnfilledVars :: Outer
-> SwapFlag
= -- see [Deferred Unification]
defer_unification outer swapped (mkTyVarTy tv1) (mkTyVarTy tv2)
-uUnfilledVars outer swapped tv1 (MetaTv info1 ref1) tv2 (SkolemTv _)
+uUnfilledVars _ swapped tv1 (MetaTv _ ref1) tv2 (SkolemTv _)
= checkUpdateMeta swapped tv1 ref1 (mkTyVarTy tv2) >> return IdCo
-uUnfilledVars outer swapped tv1 (SkolemTv _) tv2 (MetaTv info2 ref2)
+uUnfilledVars _ swapped tv1 (SkolemTv _) tv2 (MetaTv _ ref2)
= checkUpdateMeta (not swapped) tv2 ref2 (mkTyVarTy tv1) >> return IdCo
-- ToDo: this function seems too long for what it acutally does!
-uUnfilledVars outer swapped tv1 (MetaTv info1 ref1) tv2 (MetaTv info2 ref2)
+uUnfilledVars _ swapped tv1 (MetaTv info1 ref1) tv2 (MetaTv info2 ref2)
= case (info1, info2) of
(BoxTv, BoxTv) -> box_meets_box >> return IdCo
refineBoxToTau :: TcType -> TcM TcType
-- Unbox the outer box of a boxy type, filling with a monotype if it is empty
-- Like refineBox except for the "fill with monotype" part.
-refineBoxToTau ty@(TyVarTy box_tv)
+refineBoxToTau (TyVarTy box_tv)
| isMetaTyVar box_tv
, MetaTv BoxTv ref <- tcTyVarDetails box_tv
= do { cts <- readMutVar ref
| otherwise -- Skolems, and meta-tau-variables
= return (TyVarTy tv)
+unBoxPred :: PredType -> TcM PredType
unBoxPred (ClassP cls tys) = do { tys' <- mapM unBox tys; return (ClassP cls tys') }
unBoxPred (IParam ip ty) = do { ty' <- unBox ty; return (IParam ip ty') }
unBoxPred (EqPred ty1 ty2) = do { ty1' <- unBox ty1; ty2' <- unBox ty2; return (EqPred ty1' ty2') }
popUnifyCtxt (Unify False _ _) thing = thing
-----------------------
+unifyCtxt :: TcType -> TcType -> TidyEnv -> TcM (TidyEnv, SDoc)
unifyCtxt act_ty exp_ty tidy_env
= do { act_ty' <- zonkTcType act_ty
; exp_ty' <- zonkTcType exp_ty
; return (env2, mkExpectedActualMsg act_ty'' exp_ty'') }
----------------
+mkExpectedActualMsg :: Type -> Type -> SDoc
mkExpectedActualMsg act_ty exp_ty
= nest 2 (vcat [ text "Expected type" <> colon <+> ppr exp_ty,
text "Inferred type" <> colon <+> ppr act_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 :: InstOrigin -> TcType -> TcType -> TcM a -> TcM a
addSubCtxt orig actual_res_ty expected_res_ty thing_inside
= addErrCtxtM mk_err thing_inside
where
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''
+ _ -> mkExpectedActualMsg act_ty'' exp_ty''
; return (env2, message) }
wrongArgsCtxt too_many_or_few fun
<+> ptext (sLit "arguments")
------------------
+unifyForAllCtxt :: [TyVar] -> Type -> Type -> TidyEnv -> TcM (TidyEnv, SDoc)
unifyForAllCtxt tvs phi1 phi2 env
= return (env2, msg)
where
; writeKindVar kv1 k2'' }
----------------
+kindOccurCheck :: TyVar -> Type -> TcM ()
kindOccurCheck kv1 k2 -- k2 is zonked
= checkTc (not_in k2) (kindOccurCheckErr kv1 k2)
where
- not_in (TyVarTy kv2) = kv1 /= kv2
+ not_in (TyVarTy kv2) = kv1 /= kv2
not_in (FunTy a2 r2) = not_in a2 && not_in r2
- not_in other = True
+ not_in _ = True
kindSimpleKind :: Bool -> Kind -> TcM SimpleKind
-- (kindSimpleKind True k) returns a simple kind sk such that sk <: k
-- If the flag is False, it requires k <: sk
-- E.g. kindSimpleKind False ?? = *
--- What about (kv -> *) :=: ?? -> *
+-- What about (kv -> *) ~ ?? -> *
kindSimpleKind orig_swapped orig_kind
= go orig_swapped orig_kind
where
go True k
| isOpenTypeKind k = return liftedTypeKind
| isArgTypeKind k = return liftedTypeKind
- go sw k
+ go _ k
| isLiftedTypeKind k = return liftedTypeKind
| isUnliftedTypeKind k = return unliftedTypeKind
- go sw k@(TyVarTy _) = return k -- KindVars are always simple
- go swapped kind = failWithTc (ptext (sLit "Unexpected kind unification failure:")
+ go _ k@(TyVarTy _) = return k -- KindVars are always simple
+ go _ _ = failWithTc (ptext (sLit "Unexpected kind unification failure:")
<+> ppr orig_swapped <+> ppr orig_kind)
-- I think this can't actually happen
-- T v w = MkT (v -> w) v must not be an umboxed tuple
----------------
+kindOccurCheckErr :: Var -> Type -> SDoc
kindOccurCheckErr tyvar ty
= hang (ptext (sLit "Occurs check: cannot construct the infinite kind:"))
2 (sep [ppr tyvar, char '=', ppr ty])
; return (Just (arg_kind,res_kind)) }
unifyFunKind (FunTy arg_kind res_kind) = return (Just (arg_kind,res_kind))
-unifyFunKind other = return Nothing
-\end{code}
-
-%************************************************************************
-%* *
- Checking kinds
-%* *
-%************************************************************************
-
----------------------------
--- We would like to get a decent error message from
--- (a) Under-applied type constructors
--- f :: (Maybe, Maybe)
--- (b) Over-applied type constructors
--- f :: Int x -> Int x
---
-
-\begin{code}
-checkExpectedKind :: Outputable a => a -> TcKind -> TcKind -> TcM ()
--- A fancy wrapper for 'unifyKind', which tries
--- to give decent error messages.
--- (checkExpectedKind ty act_kind exp_kind)
--- checks that the actual kind act_kind is compatible
--- with the expected kind exp_kind
--- 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
- = 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
- 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)
+unifyFunKind _ = return Nothing
\end{code}
%************************************************************************
-> [TcTyVar] -- Universally-quantified type variables in the signature
-- Guaranteed to be skolems
-> TcM ()
-check_sig_tyvars extra_tvs []
+check_sig_tyvars _ []
= return ()
check_sig_tyvars extra_tvs sig_tvs
- = ASSERT( all isSkolemTyVar sig_tvs )
+ = ASSERT( all isTcTyVar sig_tvs && all isSkolemTyVar sig_tvs )
do { gbl_tvs <- tcGetGlobalTyVars
; traceTc (text "check_sig_tyvars" <+> (vcat [text "sig_tys" <+> ppr sig_tvs,
text "gbl_tvs" <+> ppr gbl_tvs,
; return (tidy_env1, escape_msg sig_tv zonked_tv globs : msgs) }
-----------------------
+escape_msg :: Var -> Var -> [SDoc] -> SDoc
escape_msg sig_tv zonked_tv globs
| notNull globs
= vcat [sep [msg, ptext (sLit "is mentioned in the environment:")],
projects / ghc-hetmet.git / blobdiff