- (arg_prefix, arg_ids)
- | isVanillaDataCon data_con -- Instantiate from commmon base
- = ([], mkTemplateLocalsNum arg_base (dataConInstOrigArgTys data_con res_tys))
- | otherwise -- The case pattern binds type variables, which are used
- -- in the types of the arguments of the pattern
- = (dc_tvs ++ mkTemplateLocalsNum arg_base (mkPredTys dc_theta),
- mkTemplateLocalsNum arg_base' dc_arg_tys)
-
- (pre_dc_tvs, pre_dc_theta, dc_arg_tys) = dataConSig data_con
- -- again we need to pull the EqPreds out of dc_theta, into dc_tvs
- dc_eqvars = map (mkWildCoVar . mkPredTy . fixEqPred) (filter isEqPred pre_dc_theta)
- -- The type of the record selector Id does not contain the univ tvs
- -- but rather their substitution according to the eq_spec. Therefore
- -- the coercion arguments bound in the case alternative will just
- -- have reflexive coercion kinds
- fixEqPred (EqPred ty1 ty2) = EqPred ty2 ty2
- dc_tvs = drop (length (dataConUnivTyVars data_con)) pre_dc_tvs ++ dc_eqvars
- dc_theta = filter (not . isEqPred) pre_dc_theta
- arg_base' = arg_base + length dc_theta
-
- unpack_base = arg_base' + length dc_arg_tys
- uniqs = map mkBuiltinUnique [unpack_base..]
-
- the_arg_id = assoc "mkRecordSelId:mk_alt" (field_lbls `zip` arg_ids) field_label
+ -- get pattern binders with types appropriately instantiated
+ arg_uniqs = map mkBuiltinUnique [arg_base..]
+ (ex_tvs, co_tvs, arg_vs) = dataConOrigInstPat arg_uniqs data_con res_tys
+
+ rebox_base = arg_base + length ex_tvs + length co_tvs + length arg_vs
+ rebox_uniqs = map mkBuiltinUnique [rebox_base..]
+
+ -- data T :: *->* where T1 { fld :: Maybe b } -> T [b]
+ -- Hence T1 :: forall a b. (a=[b]) => b -> T a
+ -- fld :: forall b. T [b] -> Maybe b
+ -- fld = /\b.\(t:T[b]). case t of
+ -- T1 b' (c : [b]=[b']) (x:Maybe b')
+ -- -> x `cast` Maybe (sym (right c))
+
+ Succeeded refinement = gadtRefine emptyRefinement ex_tvs co_tvs
+ (co_fn, res_ty) = refineType refinement (idType the_arg_id)
+ -- Generate the refinement for b'=b,
+ -- and apply to (Maybe b'), to get (Maybe b)
+
+ rhs = case co_fn of
+ ExprCoFn co -> Cast (Var the_arg_id) co
+ id_co -> ASSERT(isIdCoercion id_co) Var the_arg_id
+
+ field_vs = filter (not . isPredTy . idType) arg_vs
+ the_arg_id = assoc "mkRecordSelId:mk_alt" (field_lbls `zip` field_vs) field_label