-----------------------
-zapToTupleTy :: Boxity -> Arity -> Expected TcType -> TcM [TcType]
-zapToTupleTy boxity arity (Check ty) = unifyTupleTy boxity arity ty
-zapToTupleTy boxity arity (Infer hole) = do { (tup_ty, arg_tys) <- new_tuple_ty boxity arity ;
- writeMutVar hole tup_ty ;
- return arg_tys }
-
-unifyTupleTy boxity arity ty@(TyVarTy tyvar)
- = getTcTyVar tyvar `thenM` \ maybe_ty ->
- case maybe_ty of
- Just ty' -> unifyTupleTy boxity arity ty'
- other -> unify_tuple_ty_help boxity arity ty
-
-unifyTupleTy boxity arity ty
- = case tcSplitTyConApp_maybe ty of
- Just (tycon, arg_tys)
- | isTupleTyCon tycon
- && tyConArity tycon == arity
- && tupleTyConBoxity tycon == boxity
- -> returnM arg_tys
- other -> unify_tuple_ty_help boxity arity ty
-
-unify_tuple_ty_help boxity arity ty
- = new_tuple_ty boxity arity `thenM` \ (tup_ty, arg_tys) ->
- unifyTauTy ty tup_ty `thenM_`
- returnM arg_tys
-
-new_tuple_ty boxity arity
- = newTyVarTys arity kind `thenM` \ arg_tys ->
- return (mkTyConApp tup_tc arg_tys, arg_tys)
+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