X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2FcoreSyn%2FCoreLint.lhs;h=394140d73b2f60a343e342ccb7a9908f6242e46f;hb=734ae260b47cc71469cffe5774dce4de002ed1ee;hp=dac753af1bdff0b73fd2429d4743869e2abf3406;hpb=feb1bbef0cb4d647059c68e7741a5a5466885332;p=ghc-hetmet.git

diff --git a/compiler/coreSyn/CoreLint.lhs b/compiler/coreSyn/CoreLint.lhs
index dac753a..394140d 100644
--- a/compiler/coreSyn/CoreLint.lhs
+++ b/compiler/coreSyn/CoreLint.lhs
@@ -19,7 +19,8 @@ import Bag
 import Literal		( literalType )
 import DataCon		( dataConRepType, dataConTyCon, dataConWorkId )
 import TysWiredIn	( tupleCon )
-import Var		( Var, Id, TyVar, idType, tyVarKind, mustHaveLocalBinding, setTyVarKind, setIdType  )
+import Var		( Var, Id, TyVar, isCoVar, idType, tyVarKind, 
+			  mustHaveLocalBinding, setTyVarKind, setIdType  )
 import VarEnv           ( lookupInScope )
 import VarSet
 import Name		( getSrcLoc )
@@ -36,8 +37,8 @@ import Type		( Type, tyVarsOfType, coreEqType,
 			  TvSubst, TvSubstEnv, mkTvSubst, setTvSubstEnv, substTy,
 			  extendTvSubst, composeTvSubst, substTyVarBndr, isInScope,
 			  getTvSubstEnv, getTvInScope, mkTyVarTy )
-import Coercion         ( Coercion, coercionKind )
-import TyCon		( isPrimTyCon )
+import Coercion         ( Coercion, coercionKind, coercionKindPredTy )
+import TyCon		( isPrimTyCon, isNewTyCon )
 import BasicTypes	( RecFlag(..), Boxity(..), isNonRec )
 import StaticFlags	( opt_PprStyle_Debug )
 import DynFlags		( DynFlags, DynFlag(..), dopt )
@@ -395,12 +396,13 @@ lintCoreArg fun_ty a@(Type arg_ty) =
 lintCoreArg fun_ty arg = 
        -- Make sure function type matches argument
   do { arg_ty <- lintCoreExpr arg
-     ; let err = mkAppMsg fun_ty arg_ty arg
+     ; let err1 =  mkAppMsg fun_ty arg_ty arg
+           err2 = mkNonFunAppMsg fun_ty arg_ty arg
      ; case splitFunTy_maybe fun_ty of
         Just (arg,res) -> 
-          do { checkTys arg arg_ty err 
+          do { checkTys arg arg_ty err1
              ; return res }
-        _ -> addErrL err }
+        _ -> addErrL err2 }
 \end{code}
 
 \begin{code}
@@ -425,11 +427,12 @@ checkKinds tyvar arg_ty
 	-- tyvar; notably this is used so that we can give
 	-- 	error :: forall a:*. String -> a
 	-- and then apply it to both boxed and unboxed types.
-  = checkL (argty_kind `isSubKind` tyvar_kind)
+  = checkL (arg_kind `isSubKind` tyvar_kind)
 	   (mkKindErrMsg tyvar arg_ty)
   where
     tyvar_kind = tyVarKind tyvar
-    argty_kind = typeKind arg_ty
+    arg_kind | isCoVar tyvar = coercionKindPredTy arg_ty
+	     | otherwise     = typeKind arg_ty
 \end{code}
 
 
@@ -495,23 +498,27 @@ lintCoreAlt scrut_ty alt_ty alt@(LitAlt lit, args, rhs) =
     lit_ty = literalType lit
 
 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)
@@ -597,6 +604,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))
@@ -799,6 +821,13 @@ mkBadAltMsg scrut_ty alt
 	   text "Scrutinee type:" <+> ppr scrut_ty,
 	   text "Alternative:" <+> pprCoreAlt alt ]
 
+mkNewTyDataConAltMsg :: Type -> CoreAlt -> Message
+mkNewTyDataConAltMsg scrut_ty alt
+  = vcat [ text "Data alternative for newtype datacon",
+	   text "Scrutinee type:" <+> ppr scrut_ty,
+	   text "Alternative:" <+> pprCoreAlt alt ]
+
+
 ------------------------------------------------------
 --	Other error messages
 
@@ -809,6 +838,13 @@ mkAppMsg fun_ty arg_ty arg
 	      hang (ptext SLIT("Arg type:")) 4 (ppr arg_ty),
 	      hang (ptext SLIT("Arg:")) 4 (ppr arg)]
 
+mkNonFunAppMsg :: Type -> Type -> CoreExpr -> Message
+mkNonFunAppMsg fun_ty arg_ty arg
+  = vcat [ptext SLIT("Non-function type in function position"),
+	      hang (ptext SLIT("Fun type:")) 4 (ppr fun_ty),
+	      hang (ptext SLIT("Arg type:")) 4 (ppr arg_ty),
+	      hang (ptext SLIT("Arg:")) 4 (ppr arg)]
+
 mkKindErrMsg :: TyVar -> Type -> Message
 mkKindErrMsg tyvar arg_ty
   = vcat [ptext SLIT("Kinds don't match in type application:"),