External Core tools: track new syntax for newtypes

[ghc-hetmet.git] / utils / ext-core / Check.hs

diff --git a/utils/ext-core/Check.hs b/utils/ext-core/Check.hs
index 4d35676..e379cd7 100644 (file)
--- a/utils/ext-core/Check.hs
+++ b/utils/ext-core/Check.hs
@@ -8,8 +8,6 @@ module Check(
 
 import Maybe
 import Control.Monad.Reader
 
 import Maybe
 import Control.Monad.Reader

--- just for printing warnings
-import System.IO.Unsafe

 
 import Core
 import Printer()
 
 import Core
 import Printer()

@@ -42,19 +40,13 @@ require :: Bool -> String -> CheckResult ()
 require False s = fail s
 require True  _ = return ()
 
 require False s = fail s
 require True  _ = return ()
 

-requireM :: CheckResult Bool -> String -> CheckResult ()
-requireM cond s =
-  do b <- cond
-     require b s
-

 {- Environments. -}
 type Tvenv = Env Tvar Kind                    -- type variables  (local only)
 type Tcenv = Env Tcon KindOrCoercion          -- type constructors
 {- Environments. -}
 type Tvenv = Env Tvar Kind                    -- type variables  (local only)
 type Tcenv = Env Tcon KindOrCoercion          -- type constructors

-type Tsenv = Env Tcon ([Tvar],Ty)             -- type synonyms

 type Cenv = Env Dcon Ty                      -- data constructors
 type Venv = Env Var Ty                               -- values
 type Menv = Env AnMname Envs                 -- modules
 type Cenv = Env Dcon Ty                      -- data constructors
 type Venv = Env Var Ty                               -- values
 type Menv = Env AnMname Envs                 -- modules

-data Envs = Envs {tcenv_::Tcenv,tsenv_::Tsenv,cenv_::Cenv,venv_::Venv} -- all the exportable envs
+data Envs = Envs {tcenv_::Tcenv,cenv_::Cenv,venv_::Venv} -- all the exportable envs

   deriving Show
 
 {- Extend an environment, checking for illegal shadowing of identifiers (for term
   deriving Show
 
 {- Extend an environment, checking for illegal shadowing of identifiers (for term

@@ -85,12 +77,12 @@ lookupM env k =
 checkModule :: Menv -> Module -> CheckRes Menv
 checkModule globalEnv (Module mn tdefs vdefgs) = 
   runReaderT 
 checkModule :: Menv -> Module -> CheckRes Menv
 checkModule globalEnv (Module mn tdefs vdefgs) = 
   runReaderT 

-    (do (tcenv, tsenv, cenv) <- mkTypeEnvs tdefs
-        (e_venv,_) <- foldM (checkVdefg True (tcenv,tsenv,eempty,cenv))
+    (do (tcenv, cenv) <- mkTypeEnvs tdefs
+        (e_venv,_) <- foldM (checkVdefg True (tcenv,eempty,cenv))

                               (eempty,eempty) 
                               vdefgs
         return (eextend globalEnv 
                               (eempty,eempty) 
                               vdefgs
         return (eextend globalEnv 

-            (mn,Envs{tcenv_=tcenv,tsenv_=tsenv,cenv_=cenv,venv_=e_venv})))
+            (mn,Envs{tcenv_=tcenv,cenv_=cenv,venv_=e_venv})))

          -- avoid name shadowing
     (mn, eremove globalEnv mn)
 
          -- avoid name shadowing
     (mn, eremove globalEnv mn)
 

@@ -100,10 +92,10 @@ checkModule globalEnv (Module mn tdefs vdefgs) =
 -- of unpleasant.
 envsModule :: Menv -> Module -> Menv
 envsModule globalEnv (Module mn tdefs vdefgs) = 
 -- of unpleasant.
 envsModule :: Menv -> Module -> Menv
 envsModule globalEnv (Module mn tdefs vdefgs) = 

-   let (tcenv, tsenv, cenv) = mkTypeEnvsNoChecking tdefs
+   let (tcenv, cenv) = mkTypeEnvsNoChecking tdefs

        e_venv               = foldr vdefgTypes eempty vdefgs in
      eextend globalEnv (mn, 
        e_venv               = foldr vdefgTypes eempty vdefgs in
      eextend globalEnv (mn, 

-             (Envs{tcenv_=tcenv,tsenv_=tsenv,cenv_=cenv,venv_=e_venv}))
+             (Envs{tcenv_=tcenv,cenv_=cenv,venv_=e_venv}))

         where vdefgTypes :: Vdefg -> Venv -> Venv
               vdefgTypes (Nonrec (Vdef (v,t,_))) e =
                              add [(v,t)] e
         where vdefgTypes :: Vdefg -> Venv -> Venv
               vdefgTypes (Nonrec (Vdef (v,t,_))) e =
                              add [(v,t)] e

@@ -115,14 +107,13 @@ envsModule globalEnv (Module mn tdefs vdefgs) =
               addOne ((Nothing,_),_) e = e
               addOne ((Just _,v),t) e  = eextend e (v,t)
 
               addOne ((Nothing,_),_) e = e
               addOne ((Just _,v),t) e  = eextend e (v,t)
 

-checkTdef0 :: (Tcenv,Tsenv) -> Tdef -> CheckResult (Tcenv,Tsenv)
-checkTdef0 (tcenv,tsenv) tdef = ch tdef
+checkTdef0 :: Tcenv -> Tdef -> CheckResult Tcenv
+checkTdef0 tcenv tdef = ch tdef

       where 
        ch (Data (m,c) tbs _) = 
            do mn <- getMname
                requireModulesEq m mn "data type declaration" tdef False
       where 
        ch (Data (m,c) tbs _) = 
            do mn <- getMname
                requireModulesEq m mn "data type declaration" tdef False

-              tcenv' <- extendM NotTv tcenv (c, Kind k)
-              return (tcenv',tsenv)
+              extendM NotTv tcenv (c, Kind k)

            where k = foldr Karrow Klifted (map snd tbs)
        ch (Newtype (m,c) coVar tbs rhs) = 
            do mn <- getMname
            where k = foldr Karrow Klifted (map snd tbs)
        ch (Newtype (m,c) coVar tbs rhs) = 
            do mn <- getMname

@@ -130,37 +121,25 @@ checkTdef0 (tcenv,tsenv) tdef = ch tdef
               tcenv' <- extendM NotTv tcenv (c, Kind k)
                -- add newtype axiom to env
                tcenv'' <- envPlusNewtype tcenv' (m,c) coVar tbs rhs
               tcenv' <- extendM NotTv tcenv (c, Kind k)
                -- add newtype axiom to env
                tcenv'' <- envPlusNewtype tcenv' (m,c) coVar tbs rhs

-              tsenv' <- case rhs of
-                          Nothing -> return tsenv
-                          Just rep -> extendM NotTv tsenv (c,(map fst tbs,rep))
-              return (tcenv'', tsenv')
+              return tcenv''

            where k = foldr Karrow Klifted (map snd tbs)
 
            where k = foldr Karrow Klifted (map snd tbs)
 

-processTdef0NoChecking :: (Tcenv,Tsenv) -> Tdef -> (Tcenv,Tsenv)
-processTdef0NoChecking (tcenv,tsenv) tdef = ch tdef
+processTdef0NoChecking :: Tcenv -> Tdef -> Tcenv
+processTdef0NoChecking tcenv tdef = ch tdef

       where 
       where 

-       ch (Data (_,c) tbs _) = (eextend tcenv (c, Kind k), tsenv)
+       ch (Data (_,c) tbs _) = eextend tcenv (c, Kind k)

            where k = foldr Karrow Klifted (map snd tbs)
        ch (Newtype tc@(_,c) coercion tbs rhs) = 
            where k = foldr Karrow Klifted (map snd tbs)
        ch (Newtype tc@(_,c) coercion tbs rhs) = 

-           let tcenv' = eextend tcenv (c, Kind k)
+           let tcenv' = eextend tcenv (c, Kind k) in

                 -- add newtype axiom to env
                 -- add newtype axiom to env

-                tcenv'' = case rhs of
-                            Just rep ->
-                              eextend tcenv' 
-                               (snd coercion, Coercion $ DefinedCoercion tbs
-                                (foldl Tapp (Tcon tc) (map Tvar (fst (unzip tbs))), rep))
-                            Nothing -> tcenv'
-               tsenv' = maybe tsenv 
-                  (\ rep -> eextend tsenv (c, (map fst tbs, rep))) rhs in
-               (tcenv'', tsenv')
+                eextend tcenv'
+                  (snd coercion, Coercion $ DefinedCoercion tbs
+                    (foldl Tapp (Tcon tc) (map Tvar (fst (unzip tbs))), rhs))

            where k = foldr Karrow Klifted (map snd tbs)
 
            where k = foldr Karrow Klifted (map snd tbs)
 

-envPlusNewtype :: Tcenv -> Qual Tcon -> Qual Tcon -> [Tbind] -> Maybe Ty 
+envPlusNewtype :: Tcenv -> Qual Tcon -> Qual Tcon -> [Tbind] -> Ty

   -> CheckResult Tcenv
   -> CheckResult Tcenv

-envPlusNewtype tcenv tyCon coVar tbs rhs =
-  case rhs of
-    Nothing -> return tcenv
-    Just rep -> extendM NotTv tcenv 
+envPlusNewtype tcenv tyCon coVar tbs rep = extendM NotTv tcenv

                   (snd coVar, Coercion $ DefinedCoercion tbs
                             (foldl Tapp (Tcon tyCon) 
                                        (map Tvar (fst (unzip tbs))),
                   (snd coVar, Coercion $ DefinedCoercion tbs
                             (foldl Tapp (Tcon tyCon) 
                                        (map Tvar (fst (unzip tbs))),

@@ -187,7 +166,7 @@ checkTdef tcenv cenv = ch
                                  (foldr tArrow
                                          (foldl Tapp (Tcon (Just mn,c))
                                                 (map (Tvar . fst) utbs)) ts) tbs
                                  (foldr tArrow
                                          (foldl Tapp (Tcon (Just mn,c))
                                                 (map (Tvar . fst) utbs)) ts) tbs

-         ch (tdef@(Newtype tc _ tbs (Just t))) =  
+         ch (tdef@(Newtype tc _ tbs t)) =  

            do tvenv <- foldM (extendM Tv) eempty tbs
               kRhs <- checkTy (tcenv,tvenv) t
                require (kRhs `eqKind` Klifted) ("bad kind:\n" ++ show tdef)
            do tvenv <- foldM (extendM Tv) eempty tbs
               kRhs <- checkTy (tcenv,tvenv) t
                require (kRhs `eqKind` Klifted) ("bad kind:\n" ++ show tdef)

@@ -198,9 +177,6 @@ checkTdef tcenv cenv = ch
                     ++ " kinds: " ++
                    (show kLhs) ++ " and " ++ (show kRhs))
               return cenv
                     ++ " kinds: " ++
                    (show kLhs) ++ " and " ++ (show kRhs))
               return cenv

-        ch (Newtype _ _ _ Nothing) =
-           {- should only occur for recursive Newtypes -}
-           return cenv

 
 processCdef :: Cenv -> Tdef -> Cenv
 processCdef cenv = ch
 
 processCdef :: Cenv -> Tdef -> Cenv
 processCdef cenv = ch

@@ -217,17 +193,17 @@ processCdef cenv = ch
                                (map (Tvar . fst) utbs)) ts) tbs
     ch _ = cenv
 
                                (map (Tvar . fst) utbs)) ts) tbs
     ch _ = cenv
 

-mkTypeEnvs :: [Tdef] -> CheckResult (Tcenv, Tsenv, Cenv)
+mkTypeEnvs :: [Tdef] -> CheckResult (Tcenv, Cenv)

 mkTypeEnvs tdefs = do
 mkTypeEnvs tdefs = do

-  (tcenv, tsenv) <- foldM checkTdef0 (eempty,eempty) tdefs
+  tcenv <- foldM checkTdef0 eempty tdefs

   cenv <- foldM (checkTdef tcenv) eempty tdefs
   cenv <- foldM (checkTdef tcenv) eempty tdefs

-  return (tcenv, tsenv, cenv)
+  return (tcenv, cenv)

 
 

-mkTypeEnvsNoChecking :: [Tdef] -> (Tcenv, Tsenv, Cenv)
+mkTypeEnvsNoChecking :: [Tdef] -> (Tcenv, Cenv)

 mkTypeEnvsNoChecking tdefs = 
 mkTypeEnvsNoChecking tdefs = 

-  let (tcenv, tsenv) = foldl processTdef0NoChecking (eempty,eempty) tdefs
-      cenv           = foldl processCdef eempty tdefs in
-    (tcenv, tsenv, cenv)
+  let tcenv = foldl processTdef0NoChecking eempty tdefs
+      cenv  = foldl processCdef eempty tdefs in
+    (tcenv, cenv)

 
 requireModulesEq :: Show a => Mname -> AnMname -> String -> a 
                           -> Bool -> CheckResult ()
 
 requireModulesEq :: Show a => Mname -> AnMname -> String -> a 
                           -> Bool -> CheckResult ()

@@ -237,20 +213,20 @@ requireModulesEq Nothing _ msg t emptyOk  = require emptyOk (mkErrMsg msg t)
 mkErrMsg :: Show a => String -> a -> String
 mkErrMsg msg t = "wrong module name in " ++ msg ++ ":\n" ++ show t    
 
 mkErrMsg :: Show a => String -> a -> String
 mkErrMsg msg t = "wrong module name in " ++ msg ++ ":\n" ++ show t    
 

-checkVdefg :: Bool -> (Tcenv,Tsenv,Tvenv,Cenv) -> (Venv,Venv) 
+checkVdefg :: Bool -> (Tcenv,Tvenv,Cenv) -> (Venv,Venv)

                -> Vdefg -> CheckResult (Venv,Venv)
                -> Vdefg -> CheckResult (Venv,Venv)

-checkVdefg top_level (tcenv,tsenv,tvenv,cenv) (e_venv,l_venv) vdefg = do
+checkVdefg top_level (tcenv,tvenv,cenv) (e_venv,l_venv) vdefg = do

       mn <- getMname
       case vdefg of
        Rec vdefs ->
            do (e_venv', l_venv') <- makeEnv mn vdefs
       mn <- getMname
       case vdefg of
        Rec vdefs ->
            do (e_venv', l_venv') <- makeEnv mn vdefs

-              let env' = (tcenv,tsenv,tvenv,cenv,e_venv',l_venv')
+              let env' = (tcenv,tvenv,cenv,e_venv',l_venv')

                mapM_ (checkVdef (\ vdef k -> require (k `eqKind` Klifted) 
                         ("unlifted kind in:\n" ++ show vdef)) env') 
                      vdefs
                return (e_venv', l_venv')
        Nonrec vdef ->
                mapM_ (checkVdef (\ vdef k -> require (k `eqKind` Klifted) 
                         ("unlifted kind in:\n" ++ show vdef)) env') 
                      vdefs
                return (e_venv', l_venv')
        Nonrec vdef ->

-           do let env' = (tcenv, tsenv, tvenv, cenv, e_venv, l_venv)
+           do let env' = (tcenv, tvenv, cenv, e_venv, l_venv)

                checkVdef (\ vdef k -> do
                      require (not (k `eqKind` Kopen)) ("open kind in:\n" ++ show vdef)
                     require ((not top_level) || (not (k `eqKind` Kunlifted))) 
                checkVdef (\ vdef k -> do
                      require (not (k `eqKind` Kopen)) ("open kind in:\n" ++ show vdef)
                     require ((not top_level) || (not (k `eqKind` Kunlifted))) 

@@ -272,7 +248,7 @@ checkVdefg top_level (tcenv,tsenv,tvenv,cenv) (e_venv,l_venv) vdefg = do
          k <- checkTy (tcenv,tvenv) t
          checkKind vdef k
          t' <- checkExp env e
          k <- checkTy (tcenv,tvenv) t
          checkKind vdef k
          t' <- checkExp env e

-         requireM (equalTy tsenv t t') 
+         require (t == t')

                   ("declared type doesn't match expression type in:\n"  
                     ++ show vdef ++ "\n" ++  
                    "declared type: " ++ show t ++ "\n" ++
                   ("declared type doesn't match expression type in:\n"  
                     ++ show vdef ++ "\n" ++  
                    "declared type: " ++ show t ++ "\n" ++

@@ -285,12 +261,12 @@ vdefIsMainWrapper enclosing defining =
 checkExpr :: AnMname -> Menv -> [Tdef] -> Venv -> Tvenv 
                -> Exp -> Ty
 checkExpr mn menv tdefs venv tvenv e = case runReaderT (do
 checkExpr :: AnMname -> Menv -> [Tdef] -> Venv -> Tvenv 
                -> Exp -> Ty
 checkExpr mn menv tdefs venv tvenv e = case runReaderT (do

-  (tcenv, tsenv, cenv) <- mkTypeEnvs tdefs
+  (tcenv, cenv) <- mkTypeEnvs tdefs

   -- Since the preprocessor calls checkExpr after code has been
   -- typechecked, we expect to find the external env in the Menv.
   case (elookup menv mn) of
      Just thisEnv ->
   -- Since the preprocessor calls checkExpr after code has been
   -- typechecked, we expect to find the external env in the Menv.
   case (elookup menv mn) of
      Just thisEnv ->

-       checkExp (tcenv, tsenv, tvenv, cenv, (venv_ thisEnv), venv) e 
+       checkExp (tcenv, tvenv, cenv, (venv_ thisEnv), venv) e

      Nothing -> reportError e ("checkExpr: Environment for " ++ 
                   show mn ++ " not found")) (mn,menv) of
          OkC t -> t
      Nothing -> reportError e ("checkExpr: Environment for " ++ 
                   show mn ++ " not found")) (mn,menv) of
          OkC t -> t

@@ -298,13 +274,13 @@ checkExpr mn menv tdefs venv tvenv e = case runReaderT (do
 
 checkType :: AnMname -> Menv -> [Tdef] -> Tvenv -> Ty -> Kind
 checkType mn menv tdefs tvenv t = case runReaderT (do
 
 checkType :: AnMname -> Menv -> [Tdef] -> Tvenv -> Ty -> Kind
 checkType mn menv tdefs tvenv t = case runReaderT (do

-  (tcenv, _, _) <- mkTypeEnvs tdefs
+  (tcenv, _) <- mkTypeEnvs tdefs

   checkTy (tcenv, tvenv) t) (mn, menv) of
       OkC k -> k
       FailC s -> reportError tvenv s
 
   checkTy (tcenv, tvenv) t) (mn, menv) of
       OkC k -> k
       FailC s -> reportError tvenv s
 

-checkExp :: (Tcenv,Tsenv,Tvenv,Cenv,Venv,Venv) -> Exp -> CheckResult Ty
-checkExp (tcenv,tsenv,tvenv,cenv,e_venv,l_venv) = ch
+checkExp :: (Tcenv,Tvenv,Cenv,Venv,Venv) -> Exp -> CheckResult Ty
+checkExp (tcenv,tvenv,cenv,e_venv,l_venv) = ch

       where 
        ch e0 =
          case e0 of
       where 
        ch e0 =
          case e0 of

@@ -331,7 +307,7 @@ checkExp (tcenv,tsenv,tvenv,cenv,e_venv,l_venv) = ch
                 t2 <- ch e2
                 case t1 of
                   Tapp(Tapp(Tcon tc) t') t0 | tc == tcArrow ->
                 t2 <- ch e2
                 case t1 of
                   Tapp(Tapp(Tcon tc) t') t0 | tc == tcArrow ->

-                       do requireM (equalTy tsenv t2 t') 
+                       do require (t2 == t')

                                    ("type doesn't match at application in:\n" ++ show e0 ++ "\n" ++ 
                                     "operator type: " ++ show t' ++ "\n" ++ 
                                     "operand type: " ++ show t2) 
                                    ("type doesn't match at application in:\n" ++ show e0 ++ "\n" ++ 
                                     "operator type: " ++ show t' ++ "\n" ++ 
                                     "operand type: " ++ show t2) 

@@ -340,7 +316,7 @@ checkExp (tcenv,tsenv,tvenv,cenv,e_venv,l_venv) = ch
                               "operator type: " ++ show t1)
            Lam (Tb tb) e ->
              do tvenv' <- extendTvenv tvenv tb 
                               "operator type: " ++ show t1)
            Lam (Tb tb) e ->
              do tvenv' <- extendTvenv tvenv tb 

-                t <- checkExp (tcenv,tsenv,tvenv',cenv,e_venv,l_venv) e 
+                t <- checkExp (tcenv,tvenv',cenv,e_venv,l_venv) e 

                 return (Tforall tb t)
            Lam (Vb (vb@(_,vt))) e ->
              do k <- checkTy (tcenv,tvenv) vt
                 return (Tforall tb t)
            Lam (Vb (vb@(_,vt))) e ->
              do k <- checkTy (tcenv,tvenv) vt

@@ -348,17 +324,17 @@ checkExp (tcenv,tsenv,tvenv,cenv,e_venv,l_venv) = ch
                         ("higher-order kind in:\n" ++ show e0 ++ "\n" ++
                          "kind: " ++ show k) 
                 l_venv' <- extendVenv l_venv vb
                         ("higher-order kind in:\n" ++ show e0 ++ "\n" ++
                          "kind: " ++ show k) 
                 l_venv' <- extendVenv l_venv vb

-                t <- checkExp (tcenv,tsenv,tvenv,cenv,e_venv,l_venv') e
+                t <- checkExp (tcenv,tvenv,cenv,e_venv,l_venv') e

                 require (not (isUtupleTy vt)) ("lambda-bound unboxed tuple in:\n" ++ show e0) 
                 return (tArrow vt t)
            Let vdefg e ->
                 require (not (isUtupleTy vt)) ("lambda-bound unboxed tuple in:\n" ++ show e0) 
                 return (tArrow vt t)
            Let vdefg e ->

-             do (e_venv',l_venv') <- checkVdefg False (tcenv,tsenv,tvenv,cenv) 
-                                        (e_venv,l_venv) vdefg 
-                checkExp (tcenv,tsenv,tvenv,cenv,e_venv',l_venv') e
+             do (e_venv',l_venv') <- checkVdefg False (tcenv,tvenv,cenv)
+                                        (e_venv,l_venv) vdefg
+                checkExp (tcenv,tvenv,cenv,e_venv',l_venv') e

            Case e (v,t) resultTy alts ->
              do t' <- ch e 
                 checkTy (tcenv,tvenv) t
            Case e (v,t) resultTy alts ->
              do t' <- ch e 
                 checkTy (tcenv,tvenv) t

-                requireM (equalTy tsenv t t') 
+                require (t == t')

                          ("scrutinee declared type doesn't match expression type in:\n" ++ show e0 ++ "\n" ++
                           "declared type: " ++ show t ++ "\n" ++
                           "expression type: " ++ show t') 
                          ("scrutinee declared type doesn't match expression type in:\n" ++ show e0 ++ "\n" ++
                           "declared type: " ++ show t ++ "\n" ++
                           "expression type: " ++ show t') 

@@ -384,9 +360,8 @@ checkExp (tcenv,tsenv,tvenv,cenv,e_venv,l_venv) = ch
                   [Adefault _] -> return ()
                   _ -> fail ("no alternatives in case:\n" ++ show e0) 
                 l_venv' <- extendVenv l_venv (v,t)
                   [Adefault _] -> return ()
                   _ -> fail ("no alternatives in case:\n" ++ show e0) 
                 l_venv' <- extendVenv l_venv (v,t)

-                t:ts <- mapM (checkAlt (tcenv,tsenv,tvenv,cenv,e_venv,l_venv') t) alts  
-                bs <- mapM (equalTy tsenv t) ts
-                require (and bs)
+                t:ts <- mapM (checkAlt (tcenv,tvenv,cenv,e_venv,l_venv') t) alts
+                require (all (== t) ts)

                         ("alternative types don't match in:\n" ++ show e0 ++ "\n" ++
                          "types: " ++ show (t:ts))
                  checkTy (tcenv,tvenv) resultTy
                         ("alternative types don't match in:\n" ++ show e0 ++ "\n" ++
                          "types: " ++ show (t:ts))
                  checkTy (tcenv,tvenv) resultTy

@@ -407,8 +382,8 @@ checkExp (tcenv,tsenv,tvenv,cenv,e_venv,l_venv) = ch
              do checkTy (tcenv,eempty) t {- external types must be closed -}
                 return t
     
              do checkTy (tcenv,eempty) t {- external types must be closed -}
                 return t
     

-checkAlt :: (Tcenv,Tsenv,Tvenv,Cenv,Venv,Venv) -> Ty -> Alt -> CheckResult Ty 
-checkAlt (env@(tcenv,tsenv,tvenv,cenv,e_venv,l_venv)) t0 = ch
+checkAlt :: (Tcenv,Tvenv,Cenv,Venv,Venv) -> Ty -> Alt -> CheckResult Ty
+checkAlt (env@(tcenv,tvenv,cenv,e_venv,l_venv)) t0 = ch

       where 
        ch a0 = 
          case a0 of 
       where 
        ch a0 = 
          case a0 of 

@@ -442,21 +417,21 @@ checkAlt (env@(tcenv,tsenv,tvenv,cenv,e_venv,l_venv)) t0 = ch
                 let (ct_res:ct_args) = map (substl (utvs++etvs') (uts++(map Tvar etvs))) (ct_res0:ct_args0)
                 zipWithM_ 
                    (\ct_arg vt -> 
                 let (ct_res:ct_args) = map (substl (utvs++etvs') (uts++(map Tvar etvs))) (ct_res0:ct_args0)
                 zipWithM_ 
                    (\ct_arg vt -> 

-                       requireM (equalTy tsenv ct_arg vt)
+                       require (ct_arg == vt)

                                 ("pattern variable type doesn't match constructor argument type in:\n" ++ show a0 ++ "\n" ++
                                  "pattern variable type: " ++ show ct_arg ++ "\n" ++
                                  "constructor argument type: " ++ show vt)) ct_args vts
                                 ("pattern variable type doesn't match constructor argument type in:\n" ++ show a0 ++ "\n" ++
                                  "pattern variable type: " ++ show ct_arg ++ "\n" ++
                                  "constructor argument type: " ++ show vt)) ct_args vts

-                requireM (equalTy tsenv ct_res t0)
+                require (ct_res == t0)

                          ("pattern constructor type doesn't match scrutinee type in:\n" ++ show a0 ++ "\n" ++
                           "pattern constructor type: " ++ show ct_res ++ "\n" ++
                           "scrutinee type: " ++ show t0) 
                 l_venv' <- foldM extendVenv l_venv vbs
                          ("pattern constructor type doesn't match scrutinee type in:\n" ++ show a0 ++ "\n" ++
                           "pattern constructor type: " ++ show ct_res ++ "\n" ++
                           "scrutinee type: " ++ show t0) 
                 l_venv' <- foldM extendVenv l_venv vbs

-                t <- checkExp (tcenv,tsenv,tvenv',cenv,e_venv,l_venv') e 
+                t <- checkExp (tcenv,tvenv',cenv,e_venv,l_venv') e

                 checkTy (tcenv,tvenv) t  {- check that existentials don't escape in result type -}
                 return t
            Alit l e ->
              do t <- checkLit l
                 checkTy (tcenv,tvenv) t  {- check that existentials don't escape in result type -}
                 return t
            Alit l e ->
              do t <- checkLit l

-                requireM (equalTy tsenv t t0)
+                require (t == t0)

                         ("pattern type doesn't match scrutinee type in:\n" ++ show a0 ++ "\n" ++
                          "pattern type: " ++ show t ++ "\n" ++
                          "scrutinee type: " ++ show t0) 
                         ("pattern type doesn't match scrutinee type in:\n" ++ show a0 ++ "\n" ++
                          "pattern type: " ++ show t ++ "\n" ++
                          "scrutinee type: " ++ show t0) 

@@ -487,20 +462,10 @@ checkTy es@(tcenv,tvenv) = ch
                      let (tvs, tks) = unzip tbs
                      argKs <- mapM (checkTy es) tys
                      let kPairs = zip argKs tks
                      let (tvs, tks) = unzip tbs
                      argKs <- mapM (checkTy es) tys
                      let kPairs = zip argKs tks

-                     let kindsOk = all (uncurry eqKind) kPairs
-                     if not kindsOk &&
-                        all (uncurry subKindOf) kPairs
-                       -- GHC occasionally generates code like:
-                       -- :Co:TTypeable2 (->)
-                       -- where in this case, :Co:TTypeable2 expects an
-                       -- argument of kind (*->(*->*)) and (->) has kind
-                       -- (?->(?->*)). I'm not sure whether or not it's
-                       -- sound to apply an arbitrary coercion to an
-                       -- argument that's a subkind of what it expects.
-                       then warn $ "Applying coercion " ++ show tc ++
-                               " to arguments of kind " ++ show argKs
-                               ++ " when it expects: " ++ show tks
-                       else require kindsOk
+                         -- Simon says it's okay for these to be
+                         -- subkinds
+                     let kindsOk = all (uncurry subKindOf) kPairs
+                     require kindsOk

                         ("Kind mismatch in coercion app: " ++ show tks 
                          ++ " and " ++ show argKs ++ " t = " ++ show t)
                      return $ Keq (substl tvs tys from) (substl tvs tys to)
                         ("Kind mismatch in coercion app: " ++ show tks 
                          ++ " and " ++ show argKs ++ " t = " ++ show t)
                      return $ Keq (substl tvs tys from) (substl tvs tys to)

@@ -574,16 +539,10 @@ checkTyCo es@(tcenv,_) t@(Tapp t1 t2) =
            let (tvs, tks) = unzip tbs
            argKs <- mapM (checkTy es) tys
            let kPairs = zip argKs tks
            let (tvs, tks) = unzip tbs
            argKs <- mapM (checkTy es) tys
            let kPairs = zip argKs tks

-           let kindsOk = all (uncurry eqKind) kPairs
-           if not kindsOk &&
-                        all (uncurry subKindOf) kPairs
-                       -- see comments in checkTy about this
-                       then warn $ "Applying coercion " ++ show tc ++
-                               " to arguments of kind " ++ show argKs
-                               ++ " when it expects: " ++ show tks
-                       else require kindsOk
-                        ("Kind mismatch in coercion app: " ++ show tks 
-                         ++ " and " ++ show argKs ++ " t = " ++ show t)
+           let kindsOk = all (uncurry subKindOf) kPairs
+           require kindsOk
+              ("Kind mismatch in coercion app: " ++ show tks 
+                 ++ " and " ++ show argKs ++ " t = " ++ show t)

            return (substl tvs tys from, substl tvs tys to)
          _ -> checkTapp t1 t2
     _ -> checkTapp t1 t2)
            return (substl tvs tys from, substl tvs tys to)
          _ -> checkTapp t1 t2
     _ -> checkTapp t1 t2)

@@ -605,54 +564,6 @@ checkTyCo es t = do
     -- otherwise, expand by the "refl" rule
     _          -> return (t, t)
 
     -- otherwise, expand by the "refl" rule
     _          -> return (t, t)
 

-{- Type equality modulo newtype synonyms. -}
-equalTy :: Tsenv -> Ty -> Ty -> CheckResult Bool
-equalTy tsenv t1 t2 = 
-           do t1' <- expand t1
-              t2' <- expand t2
-              return (t1' == t2')
-      where expand (Tvar v) = return (Tvar v)
-           expand (Tcon qtc) = return (Tcon qtc)
-           expand (Tapp t1 t2) = 
-             do t2' <- expand t2
-                expapp t1 [t2']
-           expand (Tforall tb t) = 
-             do t' <- expand t
-                return (Tforall tb t')
-            expand (TransCoercion t1 t2) = do
-               exp1 <- expand t1
-               exp2 <- expand t2
-               return $ TransCoercion exp1 exp2
-            expand (SymCoercion t) = do
-               exp <- expand t
-               return $ SymCoercion exp
-            expand (UnsafeCoercion t1 t2) = do
-               exp1 <- expand t1
-               exp2 <- expand t2
-               return $ UnsafeCoercion exp1 exp2
-            expand (LeftCoercion t1) = do
-               exp1 <- expand t1
-               return $ LeftCoercion exp1
-            expand (RightCoercion t1) = do
-               exp1 <- expand t1
-               return $ RightCoercion exp1
-            expand (InstCoercion t1 t2) = do
-               exp1 <- expand t1
-               exp2 <- expand t2
-               return $ InstCoercion exp1 exp2
-           expapp (t@(Tcon (m,tc))) ts = 
-             do env <- mlookupM tsenv_ tsenv eempty m
-                case elookup env tc of 
-                   Just (formals,rhs) | (length formals) == (length ts) ->
-                         return (substl formals ts rhs)
-                   _ -> return (foldl Tapp t ts)
-           expapp (Tapp t1 t2) ts = 
-             do t2' <- expand t2
-                expapp t1 (t2':ts)
-           expapp t ts = 
-             do t' <- expand t
-                return (foldl Tapp t' ts)
-

 mlookupM :: (Eq a, Show a) => (Envs -> Env a b) -> Env a b -> Env a b -> Mname
           -> CheckResult (Env a b)
 mlookupM _ _ local_env    Nothing            = return local_env
 mlookupM :: (Eq a, Show a) => (Envs -> Env a b) -> Env a b -> Env a b -> Mname
           -> CheckResult (Env a b)
 mlookupM _ _ local_env    Nothing            = return local_env

@@ -755,6 +666,3 @@ primCoercionError s = error $ "Bad coercion application: " ++ show s
 reportError :: Show a => a -> String -> b
 reportError e s = error $ ("Core type error: checkExpr failed with "
                    ++ s ++ " and " ++ show e)
 reportError :: Show a => a -> String -> b
 reportError e s = error $ ("Core type error: checkExpr failed with "
                    ++ s ++ " and " ++ show e)

-
-warn :: String -> CheckResult ()
-warn s = (unsafePerformIO $ putStrLn ("WARNING: " ++ s)) `seq` return ()
\ No newline at end of file