--- 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] -- An infinite list of uniques
- -> DataCon
- -> [Type] -- Types to instantiate the universally quantified tyvars
- -> ([TyVar], [CoVar], [Id]) -- Return instantiated variables
-dataConInstPat uniqs con inst_tys
+-- These InstPat functions go here to avoid circularity between DataCon and Id
+dataConRepInstPat = dataConInstPat dataConRepArgTys (repeat (FSLIT("ipv")))
+dataConRepFSInstPat = dataConInstPat dataConRepArgTys
+dataConOrigInstPat = dataConInstPat dc_arg_tys (repeat (FSLIT("ipv")))
+ where
+ dc_arg_tys dc = map mkPredTy (dataConTheta dc) ++ dataConOrigArgTys dc
+ -- Remember to include the existential dictionaries
+
+dataConInstPat :: (DataCon -> [Type]) -- function used to find arg tys
+ -> [FastString] -- A long enough list of FSs to use for names
+ -> [Unique] -- An equally long 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 arg_fun fss 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 their types have been 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 b. (a :=: (a1,b)) =>
+-- Int -> b -> T a
+--
+-- dataConInstPat fss us T1 (a1',b') will return
+--
+-- ([a1'', b''], [c :: (a1', b'):=:(a1'', b'')], [x :: Int, y :: b''])
+--
+-- where the double-primed variables are created with the FastStrings and
+-- Uniques given as fss and us
+dataConInstPat arg_fun fss uniqs con inst_tys