X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;ds=sidebyside;f=compiler%2FcoreSyn%2FCoreLint.lhs;h=406bf90349cc9ffe33dcad6ff80500b25d135f06;hb=bf40e268d916947786c56ec38db86190854a2d2c;hp=a147ce2d7e9599d4202de308ddd6ad84f126f37c;hpb=e380d180947b309f6d548ddb8a3f8144c08aaff4;p=ghc-hetmet.git

diff --git a/compiler/coreSyn/CoreLint.lhs b/compiler/coreSyn/CoreLint.lhs
index a147ce2..406bf90 100644
--- a/compiler/coreSyn/CoreLint.lhs
+++ b/compiler/coreSyn/CoreLint.lhs
@@ -29,15 +29,15 @@ import ErrUtils		( dumpIfSet_core, ghcExit, Message, showPass,
 			  mkLocMessage, debugTraceMsg )
 import SrcLoc		( SrcLoc, noSrcLoc, mkSrcSpan )
 import Type		( Type, tyVarsOfType, coreEqType,
-			  splitFunTy_maybe, mkTyVarTys,
+			  splitFunTy_maybe, 
 			  splitForAllTy_maybe, splitTyConApp_maybe,
 			  isUnLiftedType, typeKind, mkForAllTy, mkFunTy,
 			  isUnboxedTupleType, isSubKind,
 			  substTyWith, emptyTvSubst, extendTvInScope, 
-			  TvSubst, TvSubstEnv, mkTvSubst, setTvSubstEnv, substTy,
-			  extendTvSubst, composeTvSubst, substTyVarBndr, isInScope,
-			  getTvSubstEnv, getTvInScope, mkTyVarTy )
-import Coercion         ( Coercion, coercionKind, coercionKindPredTy )
+			  TvSubst, substTy,
+			  extendTvSubst, substTyVarBndr, isInScope,
+			  getTvInScope )
+import Coercion         ( coercionKind, coercionKindPredTy )
 import TyCon		( isPrimTyCon, isNewTyCon )
 import BasicTypes	( RecFlag(..), Boxity(..), isNonRec )
 import StaticFlags	( opt_PprStyle_Debug )
@@ -416,12 +416,6 @@ lintTyApp ty arg_ty
 		; checkKinds tyvar arg_ty
 		; return (substTyWith [tyvar] [arg_ty] body) }
 
-lintTyApps fun_ty [] = return fun_ty
-
-lintTyApps fun_ty (arg_ty : arg_tys) = 
-  do { fun_ty' <- lintTyApp fun_ty arg_ty
-     ; lintTyApps fun_ty' arg_tys }
-
 checkKinds tyvar arg_ty
 	-- Arg type might be boxed for a function with an uncommitted
 	-- tyvar; notably this is used so that we can give
@@ -500,21 +494,25 @@ lintCoreAlt scrut_ty alt_ty alt@(LitAlt lit, args, rhs) =
 lintCoreAlt scrut_ty alt_ty alt@(DataAlt con, args, rhs)
   | isNewTyCon (dataConTyCon con) = addErrL (mkNewTyDataConAltMsg scrut_ty alt)
   | Just (tycon, tycon_arg_tys) <- splitTyConApp_maybe scrut_ty
-  = addLoc (CaseAlt alt) $  lintBinders args $ \ args -> 
-    
-      do	{ addLoc (CasePat alt) $ do
-	    {    -- Check the pattern
+  = addLoc (CaseAlt alt) $  do
+    {   -- First instantiate the universally quantified 
+	-- type variables of the data constructor
+      con_payload_ty <- lintCoreArgs (dataConRepType con) (map Type tycon_arg_tys)
+
+	-- And now bring the new binders into scope
+    ; lintBinders args $ \ args -> do
+    { addLoc (CasePat alt) $ do
+	  {    -- Check the pattern
 		 -- Scrutinee type must be a tycon applicn; checked by caller
 		 -- This code is remarkably compact considering what it does!
 		 -- NB: args must be in scope here so that the lintCoreArgs line works.
 	         -- NB: relies on existential type args coming *after* ordinary type args
 
-	  ; con_result_ty <- lintCoreArgs (dataConRepType con)
-					        (map Type tycon_arg_tys ++ varsToCoreExprs args)
+	  ; con_result_ty <- lintCoreArgs con_payload_ty (varsToCoreExprs args)
 	  ; checkTys con_result_ty scrut_ty (mkBadPatMsg con_result_ty scrut_ty) 
  	  }
 	       -- Check the RHS
-	; checkAltExpr rhs alt_ty }
+    ; checkAltExpr rhs alt_ty } }
 
   | otherwise	-- Scrut-ty is wrong shape
   = addErrL (mkBadAltMsg scrut_ty alt)
@@ -600,6 +598,21 @@ newtype LintM a =
 	    Bag Message ->           -- Error messages so far
 	    (Maybe a, Bag Message) } -- Result and error messages (if any)
 
+{-	Note [Type substitution]
+	~~~~~~~~~~~~~~~~~~~~~~~~
+Why do we need a type substitution?  Consider
+	/\(a:*). \(x:a). /\(a:*). id a x
+This is ill typed, because (renaming variables) it is really
+	/\(a:*). \(x:a). /\(b:*). id b x
+Hence, when checking an application, we can't naively compare x's type
+(at its binding site) with its expected type (at a use site).  So we
+rename type binders as we go, maintaining a substitution.
+
+The same substitution also supports let-type, current expressed as
+	(/\(a:*). body) ty
+Here we substitute 'ty' for 'a' in 'body', on the fly.
+-}
+
 instance Monad LintM where
   return x = LintM (\ loc subst errs -> (Just x, errs))
   fail err = LintM (\ loc subst errs -> (Nothing, addErr subst errs (text err) loc))