+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
+\end{code}
+
+
+%************************************************************************
+%* *
+ Overloaded literals
+%* *
+%************************************************************************
+
+In tcOverloadedLit we convert directly to an Int or Integer if we
+know that's what we want. This may save some time, by not
+temporarily generating overloaded literals, but it won't catch all
+cases (the rest are caught in lookupInst).
+
+\begin{code}
+tcOverloadedLit :: InstOrigin
+ -> HsOverLit Name
+ -> BoxyRhoType
+ -> TcM (HsOverLit TcId)
+tcOverloadedLit orig lit@(HsIntegral i fi) res_ty
+ | not (fi `isHsVar` fromIntegerName) -- Do not generate a LitInst for rebindable syntax.
+ -- Reason: If we do, tcSimplify will call lookupInst, which
+ -- will call tcSyntaxName, which does unification,
+ -- which tcSimplify doesn't like
+ -- ToDo: noLoc sadness
+ = do { integer_ty <- tcMetaTy integerTyConName
+ ; fi' <- tcSyntaxOp orig fi (mkFunTy integer_ty res_ty)
+ ; return (HsIntegral i (HsApp (noLoc fi') (nlHsLit (HsInteger i integer_ty)))) }
+
+ | Just expr <- shortCutIntLit i res_ty
+ = return (HsIntegral i expr)