+ subFunTys
+%* *
+%************************************************************************
+
+\begin{code}
+subFunTys :: SDoc -- Somthing like "The function f has 3 arguments"
+ -- or "The abstraction (\x.e) takes 1 argument"
+ -> Arity -- Expected # of args
+ -> BoxyRhoType -- res_ty
+ -> ([BoxySigmaType] -> BoxyRhoType -> TcM a)
+ -> TcM (ExprCoFn, a)
+-- Attempt to decompse res_ty to have enough top-level arrows to
+-- match the number of patterns in the match group
+--
+-- If (subFunTys n_args res_ty thing_inside) = (co_fn, res)
+-- and the inner call to thing_inside passes args: [a1,...,an], b
+-- then co_fn :: (a1 -> ... -> an -> b) -> res_ty
+--
+-- Note that it takes a BoxyRho type, and guarantees to return a BoxyRhoType
+
+
+{- Error messages from subFunTys
+
+ The abstraction `\Just 1 -> ...' has two arguments
+ but its type `Maybe a -> a' has only one
+
+ The equation(s) for `f' have two arguments
+ but its type `Maybe a -> a' has only one
+
+ The section `(f 3)' requires 'f' to take two arguments
+ but its type `Int -> Int' has only one
+
+ The function 'f' is applied to two arguments
+ but its type `Int -> Int' has only one
+-}
+
+
+subFunTys error_herald n_pats res_ty thing_inside
+ = loop n_pats [] res_ty
+ where
+ -- In 'loop', the parameter 'arg_tys' accumulates
+ -- the arg types so far, in *reverse order*
+ loop n args_so_far res_ty
+ | Just res_ty' <- tcView res_ty = loop n args_so_far res_ty'
+
+ loop n args_so_far res_ty
+ | isSigmaTy res_ty -- Do this first, 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'
+ ; return (gen_fn <.> co_fn, res) }
+
+ loop 0 args_so_far res_ty = do { res <- thing_inside (reverse args_so_far) res_ty
+ ; return (idCoercion, res) }
+ loop n args_so_far (FunTy arg_ty res_ty)
+ = do { (co_fn, res) <- loop (n-1) (arg_ty:args_so_far) res_ty
+ ; co_fn' <- wrapFunResCoercion [arg_ty] co_fn
+ ; return (co_fn', res) }
+
+ loop n args_so_far (TyVarTy tv)
+ | not (isImmutableTyVar tv)
+ = do { cts <- readMetaTyVar tv
+ ; case cts of
+ Indirect ty -> loop n args_so_far ty
+ Flexi -> do { (res_ty:arg_tys) <- withMetaTvs tv kinds mk_res_ty
+ ; res <- thing_inside (reverse args_so_far ++ arg_tys) res_ty
+ ; return (idCoercion, res) } }
+ where
+ mk_res_ty (res_ty' : arg_tys') = mkFunTys arg_tys' res_ty'
+ kinds = openTypeKind : take n (repeat argTypeKind)
+ -- Note argTypeKind: the args can have an unboxed type,
+ -- but not an unboxed tuple.
+
+ loop n args_so_far res_ty
+ = failWithTc (mk_msg (length args_so_far))
+
+ mk_msg n_actual
+ = error_herald <> comma $$
+ sep [ptext SLIT("but its type") <+> quotes (pprType res_ty),
+ if n_actual == 0 then ptext SLIT("has none")
+ else ptext SLIT("has only") <+> speakN n_actual]
+\end{code}
+
+\begin{code}
+----------------------
+boxySplitTyConApp :: TyCon -- T :: k1 -> ... -> kn -> *
+ -> BoxyRhoType -- Expected type (T a b c)
+ -> TcM [BoxySigmaType] -- Element types, a b c
+ -- It's used for wired-in tycons, so we call checkWiredInTyCOn
+ -- Precondition: never called with FunTyCon
+ -- Precondition: input type :: *
+
+boxySplitTyConApp tc orig_ty
+ = do { checkWiredInTyCon tc
+ ; loop (tyConArity tc) [] orig_ty }
+ where
+ loop n_req args_so_far ty
+ | Just ty' <- tcView ty = loop n_req args_so_far ty'
+
+ loop n_req args_so_far (TyConApp tycon args)
+ | tc == tycon
+ = ASSERT( n_req == length args) -- ty::*
+ return (args ++ args_so_far)
+
+ loop n_req args_so_far (AppTy fun arg)
+ = loop (n_req - 1) (arg:args_so_far) fun
+
+ loop n_req args_so_far (TyVarTy tv)
+ | not (isImmutableTyVar tv)
+ = do { cts <- readMetaTyVar tv
+ ; case cts of
+ Indirect ty -> loop n_req args_so_far ty
+ Flexi -> do { arg_tys <- withMetaTvs tv arg_kinds mk_res_ty
+ ; return (arg_tys ++ args_so_far) }
+ }
+ where
+ mk_res_ty arg_tys' = mkTyConApp tc arg_tys'
+ arg_kinds = map tyVarKind (take n_req (tyConTyVars tc))
+
+ loop _ _ _ = boxySplitFailure (mkTyConApp tc (mkTyVarTys (tyConTyVars tc))) orig_ty
+
+----------------------
+boxySplitListTy :: BoxyRhoType -> TcM BoxySigmaType -- Special case for lists
+boxySplitListTy exp_ty = do { [elt_ty] <- boxySplitTyConApp listTyCon exp_ty
+ ; return elt_ty }
+
+
+----------------------
+boxySplitAppTy :: BoxyRhoType -- Type to split: m a
+ -> TcM (BoxySigmaType, BoxySigmaType) -- Returns m, a
+-- Assumes (m: * -> k), where k is the kind of the incoming type
+-- If the incoming type is boxy, then so are the result types; and vice versa
+
+boxySplitAppTy orig_ty
+ = loop orig_ty
+ where
+ loop ty
+ | Just ty' <- tcView ty = loop ty'
+
+ loop ty
+ | Just (fun_ty, arg_ty) <- tcSplitAppTy_maybe ty
+ = return (fun_ty, arg_ty)
+
+ loop (TyVarTy tv)
+ | not (isImmutableTyVar tv)
+ = do { cts <- readMetaTyVar tv
+ ; case cts of
+ Indirect ty -> loop ty
+ Flexi -> do { [fun_ty,arg_ty] <- withMetaTvs tv kinds mk_res_ty
+ ; return (fun_ty, arg_ty) } }
+ where
+ mk_res_ty [fun_ty', arg_ty'] = mkAppTy fun_ty' arg_ty'
+ tv_kind = tyVarKind tv
+ kinds = [mkArrowKind liftedTypeKind (defaultKind tv_kind),
+ -- m :: * -> k
+ liftedTypeKind] -- arg type :: *
+ -- The defaultKind is a bit smelly. If you remove it,
+ -- try compiling f x = do { x }
+ -- and you'll get a kind mis-match. It smells, but
+ -- not enough to lose sleep over.
+
+ loop _ = boxySplitFailure (mkAppTy alphaTy betaTy) orig_ty
+
+------------------
+boxySplitFailure actual_ty expected_ty
+ = unifyMisMatch False actual_ty expected_ty
+\end{code}
+
+
+--------------------------------
+-- withBoxes: the key utility function
+--------------------------------
+
+\begin{code}
+withMetaTvs :: TcTyVar -- An unfilled-in, non-skolem, meta type variable
+ -> [Kind] -- Make fresh boxes (with the same BoxTv/TauTv setting as tv)
+ -> ([BoxySigmaType] -> BoxySigmaType)
+ -- Constructs the type to assign
+ -- to the original var
+ -> TcM [BoxySigmaType] -- Return the fresh boxes
+
+-- It's entirely possible for the [kind] to be empty.
+-- For example, when pattern-matching on True,
+-- we call boxySplitTyConApp passing a boolTyCon
+
+-- Invariant: tv is still Flexi
+
+withMetaTvs tv kinds mk_res_ty
+ | isBoxyTyVar tv
+ = do { box_tvs <- mapM (newMetaTyVar BoxTv) kinds
+ ; let box_tys = mkTyVarTys box_tvs
+ ; writeMetaTyVar tv (mk_res_ty box_tys)
+ ; return box_tys }
+
+ | otherwise -- Non-boxy meta type variable
+ = do { tau_tys <- mapM newFlexiTyVarTy kinds
+ ; writeMetaTyVar tv (mk_res_ty tau_tys) -- Write it *first*
+ -- Sure to be a tau-type
+ ; return tau_tys }
+
+withBox :: Kind -> (BoxySigmaType -> TcM a) -> TcM (a, TcType)
+-- Allocate a *boxy* tyvar
+withBox kind thing_inside
+ = do { box_tv <- newMetaTyVar BoxTv kind
+ ; res <- thing_inside (mkTyVarTy box_tv)
+ ; ty <- readFilledBox box_tv
+ ; return (res, ty) }
+\end{code}
+
+
+%************************************************************************
+%* *
+ Approximate boxy matching
+%* *
+%************************************************************************
+
+\begin{code}
+boxySubMatchType
+ :: TcTyVarSet -> TcType -- The "template"; the tyvars are skolems
+ -> BoxyRhoType -- Type to match (note a *Rho* type)
+ -> TvSubst -- Substitution of the [TcTyVar] to BoxySigmaTypes
+
+boxyMatchTypes
+ :: TcTyVarSet -> [TcType] -- The "template"; the tyvars are skolems
+ -> [BoxySigmaType] -- Type to match
+ -> TvSubst -- Substitution of the [TcTyVar] to BoxySigmaTypes
+
+-- Find a *boxy* substitution that makes the template look as much
+-- like the BoxySigmaType as possible.
+-- It's always ok to return an empty substitution;
+-- anything more is jam on the pudding
+--
+-- NB1: This is a pure, non-monadic function.
+-- It does no unification, and cannot fail
+--
+-- Note [Matching kinds]
+-- The target type might legitimately not be a sub-kind of template.
+-- For example, suppose the target is simply a box with an OpenTypeKind,
+-- and the template is a type variable with LiftedTypeKind.
+-- Then it's ok (because the target type will later be refined).
+-- We simply don't bind the template type variable.
+--
+-- It might also be that the kind mis-match is an error. For example,
+-- suppose we match the template (a -> Int) against (Int# -> Int),
+-- where the template type variable 'a' has LiftedTypeKind. This
+-- matching function does not fail; it simply doesn't bind the template.
+-- Later stuff will fail.
+--
+-- Precondition: the arg lengths are equal
+-- Precondition: none of the template type variables appear in the [BoxySigmaType]
+-- Precondition: any nested quantifiers in either type differ from
+-- the template type variables passed as arguments
+--
+-- Note [Sub-match]
+-- ~~~~~~~~~~~~~~~~
+-- Consider this
+-- head :: [a] -> a
+-- |- head xs : <rhobox>
+-- We will do a boxySubMatchType between a ~ <rhobox>
+-- But we *don't* want to match [a |-> <rhobox>] because
+-- (a) The box should be filled in with a rho-type, but
+-- but the returned substitution maps TyVars to boxy *sigma*
+-- types
+-- (b) In any case, the right final answer might be *either*
+-- instantiate 'a' with a rho-type or a sigma type
+-- head xs : Int vs head xs : forall b. b->b
+-- So the matcher MUST NOT make a choice here. In general, we only
+-- bind a template type variable in boxyMatchType, not in boxySubMatchType.
+
+boxySubMatchType tmpl_tvs tmpl_ty boxy_ty
+ = go tmpl_ty boxy_ty
+ where
+ go t_ty b_ty
+ | Just t_ty' <- tcView t_ty = go t_ty' b_ty
+ | Just b_ty' <- tcView b_ty = go t_ty b_ty'
+
+ go (FunTy arg1 res1) (FunTy arg2 res2)
+ = do_match arg1 arg2 (go res1 res2)
+ -- Match the args, and sub-match the results
+
+ go (TyVarTy _) b_ty = emptyTvSubst -- Do not bind! See Note [Sub-match]
+
+ go t_ty b_ty = do_match t_ty b_ty emptyTvSubst -- Otherwise we are safe to bind
+
+ do_match t_ty b_ty subst = boxy_match tmpl_tvs t_ty emptyVarSet b_ty subst
+
+------------
+boxyMatchTypes tmpl_tvs tmpl_tys boxy_tys
+ = ASSERT( length tmpl_tys == length boxy_tys )
+ boxy_match_s tmpl_tvs tmpl_tys emptyVarSet boxy_tys emptyTvSubst
+ -- ToDo: add error context?
+
+boxy_match_s tmpl_tvs [] boxy_tvs [] subst
+ = subst
+boxy_match_s tmpl_tvs (t_ty:t_tys) boxy_tvs (b_ty:b_tys) subst
+ = boxy_match_s tmpl_tvs t_tys boxy_tvs b_tys $
+ boxy_match tmpl_tvs t_ty boxy_tvs b_ty subst
+
+------------
+boxy_match :: TcTyVarSet -> TcType -- Template
+ -> TcTyVarSet -- boxy_tvs: do not bind template tyvars to any of these
+ -> BoxySigmaType -- Match against this type
+ -> TvSubst
+ -> TvSubst
+
+-- The boxy_tvs argument prevents this match:
+-- [a] forall b. a ~ forall b. b
+-- We don't want to bind the template variable 'a'
+-- to the quantified type variable 'b'!
+
+boxy_match tmpl_tvs orig_tmpl_ty boxy_tvs orig_boxy_ty subst
+ = go orig_tmpl_ty orig_boxy_ty
+ where
+ go t_ty b_ty
+ | Just t_ty' <- tcView t_ty = go t_ty' b_ty
+ | Just b_ty' <- tcView b_ty = go t_ty b_ty'
+
+ go (ForAllTy _ ty1) (ForAllTy tv2 ty2)
+ = boxy_match tmpl_tvs ty1 (boxy_tvs `extendVarSet` tv2) ty2 subst
+
+ go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
+ | tc1 == tc2 = go_s tys1 tys2
+
+ go (FunTy arg1 res1) (FunTy arg2 res2)
+ = go_s [arg1,res1] [arg2,res2]
+
+ go t_ty b_ty
+ | Just (s1,t1) <- tcSplitAppTy_maybe t_ty,
+ Just (s2,t2) <- tcSplitAppTy_maybe b_ty,
+ typeKind t2 `isSubKind` typeKind t1 -- Maintain invariant
+ = go_s [s1,t1] [s2,t2]
+
+ go (TyVarTy tv) b_ty
+ | tv `elemVarSet` tmpl_tvs -- Template type variable in the template
+ , not (intersectsVarSet boxy_tvs (tyVarsOfType orig_boxy_ty))
+ , typeKind b_ty `isSubKind` tyVarKind tv
+ = extendTvSubst subst tv boxy_ty'
+ where
+ boxy_ty' = case lookupTyVar subst tv of
+ Nothing -> orig_boxy_ty
+ Just ty -> ty `boxyLub` orig_boxy_ty
+
+ go _ _ = subst -- Always safe
+
+ --------
+ go_s tys1 tys2 = boxy_match_s tmpl_tvs tys1 boxy_tvs tys2 subst
+
+
+boxyLub :: BoxySigmaType -> BoxySigmaType -> BoxySigmaType
+-- Combine boxy information from the two types
+-- If there is a conflict, return the first
+boxyLub orig_ty1 orig_ty2
+ = go orig_ty1 orig_ty2
+ where
+ go (AppTy f1 a1) (AppTy f2 a2) = AppTy (boxyLub f1 f2) (boxyLub a1 a2)
+ go (FunTy f1 a1) (FunTy f2 a2) = AppTy (boxyLub f1 f2) (boxyLub a1 a2)
+ go (TyConApp tc1 ts1) (TyConApp tc2 ts2)
+ | tc1 == tc2, length ts1 == length ts2
+ = TyConApp tc1 (zipWith boxyLub ts1 ts2)
+
+ go (TyVarTy tv1) ty2 -- This is the whole point;
+ | isTcTyVar tv1, isMetaTyVar tv1 -- choose ty2 if ty2 is a box
+ = ty2
+
+ -- 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'
+
+ -- For now, we don't look inside ForAlls, PredTys
+ go ty1 ty2 = orig_ty1 -- Default
+\end{code}
+
+
+%************************************************************************
+%* *
+ Subsumption checking