- ; con_result_ty <- lintCoreArgs con_type (map Var args)
- ; checkTys con_result_ty scrut_ty (mkBadPatMsg con_result_ty scrut_ty)
- -- Check the RHS
- ; checkAltExpr rhs alt_ty } ;
- Nothing -> addErrL (mkBadAltMsg scrut_ty alt)
- } }
-
- | otherwise
- = addLoc (CaseAlt alt) $
- addInScopeVars args $ -- Put the args in scope before lintBinder, because
- -- the Ids mention the type variables
- do { mapM lintBinder args
- ; case splitTyConApp_maybe scrut_ty of {
- Nothing -> addErrL (mkBadAltMsg scrut_ty alt) ;
- Just (tycon, tycon_args_tys) ->
- do { checkL (tycon == dataConTyCon con) (mkIncTyconMsg tycon alt)
- ; pat_res_ty <- lintCoreArgs (dataConRepType con) (map varToCoreExpr args)
- ; subst <- getTvSubst
- ; case coreRefineTys args subst pat_res_ty scrut_ty of
- Just senv -> updateTvSubstEnv senv (checkAltExpr rhs alt_ty)
- Nothing -> return () -- Alternative is dead code
- } } }
+ ; con_result_ty <- lintCoreArgs con_type (map Var args)
+ ; checkTys con_result_ty scrut_ty (mkBadPatMsg con_result_ty scrut_ty)
+ }
+ -- Check the RHS
+ ; checkAltExpr rhs alt_ty }
+
+ else -- GADT
+ do { let (tvs,ids) = span isTyVar args
+ ; subst <- getTvSubst
+ ; let in_scope = getTvInScope subst
+ subst_env = getTvSubstEnv subst
+ ; case coreRefineTys in_scope con tvs scrut_ty of {
+ Nothing -> return () ; -- Alternative is dead code
+ Just (refine, _) -> updateTvSubstEnv (composeTvSubst in_scope refine subst_env) $
+ do { addLoc (CasePat alt) $ do
+ { tvs' <- mapM lintTy (mkTyVarTys tvs)
+ ; con_type <- lintTyApps (dataConRepType con) tvs'
+ ; mapM lintBinder ids -- Lint Ids in the refined world
+ ; lintCoreArgs con_type (map Var ids)
+ }
+
+ ; let refined_alt_ty = substTy (mkTvSubst in_scope refine) alt_ty
+ -- alt_ty is already an OutType, so don't re-apply
+ -- the current substitution. But we must apply the
+ -- refinement so that the check in checkAltExpr is ok
+ ; checkAltExpr rhs refined_alt_ty
+ } } }
+
+ | otherwise -- Scrut-ty is wrong shape
+ = addErrL (mkBadAltMsg scrut_ty alt)