-refineAlt :: PatState
- -> DataCon -- For tracing only
- -> [TcTyVar] -- Type variables from pattern
- -> [Bool] -- Flags indicating which type variables occur
- -- in the type of at least one argument
- -> [TcType] -- Result types from the pattern
- -> [BoxySigmaType] -- Result types from the scrutinee (context)
- -> (PatState -> [BoxySigmaType] -> TcM a)
- -- Possibly-refined existentials
- -> TcM a
-refineAlt pstate con pat_tvs arg_flags pat_res_tys ctxt_res_tys thing_inside
- | not (all isRigidTy ctxt_res_tys)
- -- The context is not a rigid type, so we do no type refinement here.
- = do { let arg_tvs = mkVarSet [ tv | (tv, True) <- pat_tvs `zip` arg_flags]
- subst = boxyMatchTypes arg_tvs pat_res_tys ctxt_res_tys
-
- res_tvs = tcTyVarsOfTypes pat_res_tys
- -- The tvs are (already) all fresh skolems. We need a
- -- fresh skolem for each type variable (to bind in the pattern)
- -- even if it's refined away by the type refinement
- find_inst tv
- | not (tv `elemVarSet` res_tvs) = return (mkTyVarTy tv)
- | Just boxy_ty <- lookupTyVar subst tv = return boxy_ty
- | otherwise = do { tv <- newBoxyTyVar openTypeKind
- ; return (mkTyVarTy tv) }
- ; pat_tys' <- mapM find_inst pat_tvs
-
- -- Do the thing inside
- ; res <- thing_inside pstate pat_tys'
-
- -- Unbox the types that have been filled in by the thing_inside
- -- I.e. the ones whose type variables are mentioned in at least one arg
- ; let strip ty in_arg_tv | in_arg_tv = stripBoxyType ty
- | otherwise = return ty
- ; pat_tys'' <- zipWithM strip pat_tys' arg_flags
- ; let subst = zipOpenTvSubst pat_tvs pat_tys''
- ; boxyUnifyList (substTys subst pat_res_tys) ctxt_res_tys
-
- ; return res } -- All boxes now filled
-
- | otherwise -- The context is rigid, so we can do type refinement
- = case gadtRefineTys (pat_reft pstate) con pat_tvs pat_res_tys ctxt_res_tys of
- Failed msg -> failWithTc (inaccessibleAlt msg)
- Succeeded (new_subst, all_bound_here)
- | all_bound_here -- All the new bindings are for pat_tvs, so no need
- -- to refine the environment or pstate
- -> do { traceTc trace_msg
- ; thing_inside pstate pat_tvs' }
- | otherwise -- New bindings affect the context, so pass down pstate'.
- -- DO NOT refine the envt, because we might be inside a
- -- lazy pattern
- -> do { traceTc trace_msg
- ; thing_inside pstate' pat_tvs' }
- where
- pat_tvs' = map (substTyVar new_subst) pat_tvs
- pstate' = pstate { pat_reft = new_subst }
- trace_msg = text "refineTypes:match" <+> ppr con <+> ppr new_subst
-
-refineType :: GadtRefinement -> BoxyRhoType -> BoxyRhoType
--- Refine the type if it is rigid
-refineType reft ty
- | isRefineableTy ty = substTy reft ty
- | otherwise = ty
+refineAlt :: DataCon -- For tracing only
+ -> PatState
+ -> [TcTyVar] -- Existentials
+ -> [CoVar] -- Equational constraints
+ -> BoxySigmaType -- Pattern type
+ -> TcM PatState
+
+refineAlt con pstate ex_tvs [] pat_ty
+ = return pstate -- Common case: no equational constraints
+
+refineAlt con pstate ex_tvs co_vars pat_ty
+ | not (isRigidTy pat_ty)
+ = failWithTc (nonRigidMatch con)
+ -- We are matching against a GADT constructor with non-trivial
+ -- constraints, but pattern type is wobbly. For now we fail.
+ -- We can make sense of this, however:
+ -- Suppose MkT :: forall a b. (a:=:[b]) => b -> T a
+ -- (\x -> case x of { MkT v -> v })
+ -- We can infer that x must have type T [c], for some wobbly 'c'
+ -- and translate to
+ -- (\(x::T [c]) -> case x of
+ -- MkT b (g::([c]:=:[b])) (v::b) -> v `cast` sym g
+ -- To implement this, we'd first instantiate the equational
+ -- constraints with *wobbly* type variables for the existentials;
+ -- then unify these constraints to make pat_ty the right shape;
+ -- then proceed exactly as in the rigid case
+
+ | otherwise -- In the rigid case, we perform type refinement
+ = case gadtRefine (pat_reft pstate) ex_tvs co_vars of {
+ Failed msg -> failWithTc (inaccessibleAlt msg) ;
+ Succeeded reft -> do { traceTc trace_msg
+ ; return (pstate { pat_reft = reft }) }
+ -- DO NOT refine the envt right away, because we
+ -- might be inside a lazy pattern. Instead, refine pstate
+ where
+
+ trace_msg = text "refineAlt:match" <+> ppr con <+> ppr reft
+ }