+-- deep applies a TyConApp coercion as a substitution to a reflexive coercion
+-- deepCast t [a1,...,an] co corresponds to deep(t, [a1,...,an], co) from
+-- FC paper
+deepCast :: Type -> [TyVar] -> Coercion -> Coercion
+deepCast ty tyVars co
+ = ASSERT( let {(lty, rty) = coercionKind co;
+ Just (tc1, lArgs) = splitTyConApp_maybe lty;
+ Just (tc2, rArgs) = splitTyConApp_maybe rty}
+ in
+ tc1 == tc2 && length lArgs == length rArgs &&
+ length lArgs == length tyVars )
+ substTyWith tyVars coArgs ty
+ where
+ -- coArgs = [right (left (left co)), right (left co), right co]
+ coArgs = decomposeCo (length tyVars) co
+
+-- This goes here to avoid circularity between DataCon and Id
+dataConInstPat :: [Unique] -- A long enough list of uniques, at least one for each binder
+ -> DataCon
+ -> [Type] -- Types to instantiate the universally quantified tyvars
+ -> ([TyVar], [CoVar], [Id]) -- Return instantiated variables
+-- dataConInstPat us con inst_tys returns a triple (ex_tvs, co_tvs, arg_ids),
+--
+-- ex_tvs are intended to be used as binders for existential type args
+--
+-- co_tvs are intended to be used as binders for coercion args and the kinds
+-- of these vars have been instantiated by the inst_tys and the ex_tys
+--
+-- arg_ids are indended to be used as binders for value arguments, including
+-- dicts, and have their types instantiated with inst_tys and ex_tys
+--
+-- Example.
+-- The following constructor T1
+--
+-- data T a where
+-- T1 :: forall b. Int -> b -> T(a,b)
+-- ...
+--
+-- has representation type
+-- forall a. forall a1. forall a2. forall b. (a :=: (a1,a2)) =>
+-- Int -> b -> T a
+--
+-- dataConInstPat us T1 (a1',a2') will return
+--
+-- ([a1'', a2'', b''],[c :: (a1',a2'):=:(a1'',a2'')],[x :: Int,y :: b''])
+--
+-- where the double-primed variables are created from the unique list input
+dataConInstPat uniqs con inst_tys
+ = dataConOccInstPat uniqs occs con inst_tys
+ where
+ -- dataConOccInstPat doesn't actually make use of the OccName directly for
+ -- existential and coercion variable binders, so it is right to just
+ -- use the VarName namespace for all of the OccNames
+ occs = mk_occs 1
+ mk_occs n = mkVarOcc ("ipv" ++ show n) : mk_occs (n+1)
+
+dataConOccInstPat :: [Unique] -- A long enough list of uniques, at least one for each binder
+ -> [OccName] -- An equally long list of OccNames to use
+ -> DataCon
+ -> [Type] -- Types to instantiate the universally quantified tyvars
+ -> ([TyVar], [CoVar], [Id]) -- Return instantiated variables
+-- This function actually does the job specified in the comment for
+-- dataConInstPat, but uses the specified list of OccNames. This is
+-- is necessary for use in e.g. tcIfaceDataAlt
+dataConOccInstPat uniqs occs con inst_tys
+ = (ex_bndrs, co_bndrs, id_bndrs)
+ where
+ univ_tvs = dataConUnivTyVars con
+ ex_tvs = dataConExTyVars con
+ arg_tys = dataConRepArgTys con
+ eq_spec = dataConEqSpec con
+ eq_preds = [ mkEqPred (mkTyVarTy tv, ty) | (tv,ty) <- eq_spec ]
+
+ n_ex = length ex_tvs
+ n_co = length eq_spec
+ n_id = length arg_tys
+
+ -- split the Uniques and OccNames
+ (ex_uniqs, uniqs') = splitAt n_ex uniqs
+ (co_uniqs, id_uniqs) = splitAt n_co uniqs'
+
+ (ex_occs, occs') = splitAt n_ex occs
+ (co_occs, id_occs) = splitAt n_co occs'
+
+ -- make existential type variables
+ mk_ex_var uniq occ var = mkTyVar new_name kind
+ where
+ new_name = mkSysTvName uniq (occNameFS occ)
+ kind = tyVarKind var
+
+ ex_bndrs = zipWith3 mk_ex_var ex_uniqs ex_occs ex_tvs
+
+ -- make the instantiation substitution
+ inst_subst = substTyWith (univ_tvs ++ ex_tvs) (inst_tys ++ map mkTyVarTy ex_bndrs)
+
+ -- make new coercion vars, instantiating kind
+ mk_co_var uniq occ eq_pred = mkCoVar new_name (inst_subst (mkPredTy eq_pred))
+ where
+ new_name = mkSysTvName uniq (occNameFS occ)
+
+ co_bndrs = zipWith3 mk_co_var co_uniqs co_occs eq_preds
+
+ -- make value vars, instantiating types
+ mk_id_var uniq occ ty = mkUserLocal occ uniq (inst_subst ty) noSrcLoc
+ id_bndrs = zipWith3 mk_id_var id_uniqs id_occs arg_tys
+