utils/ext-core/Language/Core/Check.hs

   1 {-# OPTIONS -Wall -fno-warn-name-shadowing #-}
   2 module Language.Core.Check(
   3   checkModule, envsModule,
   4   checkExpr, checkType,
   5   primCoercionError,
   6   Menv, Venv, Tvenv, Envs(..),
   7   CheckRes(..), splitTy, substl,
   8   mkTypeEnvsNoChecking, NtEnv, mkNtEnv) where
   9
  10 --import Debug.Trace
  11
  12 import Language.Core.Core
  13 import Language.Core.CoreUtils
  14 import Language.Core.Printer()
  15 import Language.Core.PrimEnv
  16 import Language.Core.Env
  17 import Language.Core.Environments
  18
  19 import Control.Monad.Reader
  20 import Data.List
  21 import qualified Data.Map as M
  22 import Data.Maybe
  23
  24 {- Checking is done in a simple error monad.  In addition to
  25    allowing errors to be captured, this makes it easy to guarantee
  26    that checking itself has been completed for an entire module. -}
  27
  28 {- We use the Reader monad transformer in order to thread the
  29    top-level module name throughout the computation simply.
  30    This is so that checkExp can also be an entry point (we call it
  31    from Prep.) -}
  32 data CheckRes a = OkC a | FailC String
  33 type CheckResult a = ReaderT (AnMname, Menv) CheckRes a
  34 getMname :: CheckResult AnMname
  35 getMname     = ask >>= (return . fst)
  36 getGlobalEnv :: CheckResult Menv
  37 getGlobalEnv = ask >>= (return . snd)
  38
  39 instance Monad CheckRes where
  40   OkC a >>= k = k a
  41   FailC s >>= _ = fail s
  42   return = OkC
  43   fail = FailC
  44
  45 require :: Bool -> String -> CheckResult ()
  46 require False s = fail s
  47 require True  _ = return ()
  48
  49
  50 extendM :: (Ord a, Show a) => Bool -> EnvType -> Env a b -> (a,b) -> CheckResult (Env a b)
  51 extendM checkNameShadowing envType env (k,d) =
  52    case elookup env k of
  53      Just _ | envType == NotTv && checkNameShadowing -> fail ("multiply-defined identifier: "
  54                                       ++ show k)
  55      _ -> return (eextend env (k,d))
  56
  57 extendVenv :: (Ord a, Show a) => Bool -> Env a b -> (a,b) -> CheckResult (Env a b)
  58 extendVenv check = extendM check NotTv
  59
  60 extendTvenv :: (Ord a, Show a) => Env a b -> (a,b) -> CheckResult (Env a b)
  61 extendTvenv = extendM True Tv
  62
  63 lookupM :: (Ord a, Show a) => Env a b -> a -> CheckResult (Maybe b)
  64 lookupM env k = return $ elookup env k
  65
  66 {- Main entry point. -}
  67 checkModule :: Menv -> Module -> CheckRes Menv
  68 checkModule globalEnv (Module mn tdefs vdefgs) =
  69   runReaderT
  70     (do (tcenv, cenv) <- mkTypeEnvs tdefs
  71         (e_venv,_) <- foldM (checkVdefg True (tcenv,eempty,cenv))
  72                               (eempty,eempty)
  73                               vdefgs
  74         return (eextend globalEnv
  75             (mn,Envs{tcenv_=tcenv,cenv_=cenv,venv_=e_venv})))
  76     (mn, globalEnv)
  77
  78 -- Like checkModule, but doesn't typecheck the code, instead just
  79 -- returning declared types for top-level defns.
  80 -- This is necessary in order to handle circular dependencies, but it's sort
  81 -- of unpleasant.
  82 envsModule :: Menv -> Module -> Menv
  83 envsModule globalEnv (Module mn tdefs vdefgs) =
  84    let (tcenv, cenv) = mkTypeEnvsNoChecking tdefs
  85        e_venv               = foldr vdefgTypes eempty vdefgs in
  86      eextend globalEnv (mn,
  87              (Envs{tcenv_=tcenv,cenv_=cenv,venv_=e_venv}))
  88         where vdefgTypes :: Vdefg -> Venv -> Venv
  89               vdefgTypes (Nonrec (Vdef (v,t,_))) e =
  90                              add [(v,t)] e
  91               vdefgTypes (Rec vds) e =
  92                              add (map (\ (Vdef (v,t,_)) -> (v,t)) vds) e
  93               add :: [(Qual Var,Ty)] -> Venv -> Venv
  94               add pairs e = foldr addOne e pairs
  95               addOne :: (Qual Var, Ty) -> Venv -> Venv
  96               addOne ((_,v),t) e  = eextend e (v,t)
  97
  98 checkTdef0 :: Tcenv -> Tdef -> CheckResult Tcenv
  99 checkTdef0 tcenv tdef = ch tdef
 100       where
 101         ch (Data (m,c) tbs _) =
 102             do mn <- getMname
 103                requireModulesEq m mn "data type declaration" tdef False
 104                extendM True NotTv tcenv (c, Kind k)
 105             where k = foldr Karrow Klifted (map snd tbs)
 106         ch (Newtype (m,c) coVar tbs rhs) =
 107             do mn <- getMname
 108                requireModulesEq m mn "newtype declaration" tdef False
 109                tcenv' <- extendM True NotTv tcenv (c, Kind k)
 110                -- add newtype axiom to env
 111                tcenv'' <- envPlusNewtype tcenv' (m,c) coVar tbs rhs
 112                return tcenv''
 113             where k = foldr Karrow Klifted (map snd tbs)
 114
 115 processTdef0NoChecking :: Tcenv -> Tdef -> Tcenv
 116 processTdef0NoChecking tcenv tdef = ch tdef
 117       where
 118         ch (Data (_,c) tbs _) = eextend tcenv (c, Kind k)
 119             where k = foldr Karrow Klifted (map snd tbs)
 120         ch (Newtype tc@(_,c) coercion tbs rhs) =
 121             let tcenv' = eextend tcenv (c, Kind k) in
 122                 -- add newtype axiom to env
 123                 eextend tcenv'
 124                   (snd coercion, Coercion $ DefinedCoercion tbs
 125                     (foldl Tapp (Tcon tc) (map Tvar (fst (unzip tbs))), rhs))
 126             where k = foldr Karrow Klifted (map snd tbs)
 127
 128 envPlusNewtype :: Tcenv -> Qual Tcon -> Qual Tcon -> [Tbind] -> Ty
 129   -> CheckResult Tcenv
 130 envPlusNewtype tcenv tyCon coVar tbs rep = extendM True NotTv tcenv
 131                   (snd coVar, Coercion $ DefinedCoercion tbs
 132                             (foldl Tapp (Tcon tyCon)
 133                                        (map Tvar (fst (unzip tbs))),
 134                                        rep))
 135
 136 checkTdef :: Tcenv -> Cenv -> Tdef -> CheckResult Cenv
 137 checkTdef tcenv cenv = ch
 138        where
 139          ch (Data (_,c) utbs cdefs) =
 140             do cbinds <- mapM checkCdef cdefs
 141                foldM (extendM True NotTv) cenv cbinds
 142             where checkCdef (cdef@(Constr (m,dcon) etbs ts)) =
 143                     do mn <- getMname
 144                        requireModulesEq m mn "constructor declaration" cdef
 145                          False
 146                        tvenv <- foldM (extendM True Tv) eempty tbs
 147                        ks <- mapM (checkTy (tcenv,tvenv)) ts
 148                        mapM_ (\k -> require (baseKind k)
 149                                             ("higher-order kind in:\n" ++ show cdef ++ "\n" ++
 150                                              "kind: " ++ show k) ) ks
 151                        return (dcon,t mn)
 152                     where tbs = utbs ++ etbs
 153                           t mn = foldr Tforall
 154                                   (foldr tArrow
 155                                           (foldl Tapp (Tcon (Just mn,c))
 156                                                  (map (Tvar . fst) utbs)) ts) tbs
 157          ch (tdef@(Newtype tc _ tbs t)) =
 158             do tvenv <- foldM (extendM True Tv) eempty tbs
 159                kRhs <- checkTy (tcenv,tvenv) t
 160                require (kRhs `eqKind` Klifted) ("bad kind:\n" ++ show tdef)
 161                kLhs <- checkTy (tcenv,tvenv)
 162                          (foldl Tapp (Tcon tc) (map Tvar (fst (unzip tbs))))
 163                require (kLhs `eqKind` kRhs)
 164                   ("Kind mismatch in newtype axiom types: " ++ show tdef
 165                     ++ " kinds: " ++
 166                    (show kLhs) ++ " and " ++ (show kRhs))
 167                return cenv
 168
 169 processCdef :: Cenv -> Tdef -> Cenv
 170 processCdef cenv = ch
 171   where
 172     ch (Data (_,c) utbs cdefs) = do
 173        let cbinds = map checkCdef cdefs
 174        foldl eextend cenv cbinds
 175      where checkCdef (Constr (mn,dcon) etbs ts) =
 176              (dcon,t mn)
 177             where tbs = utbs ++ etbs
 178                   t mn = foldr Tforall
 179                           (foldr tArrow
 180                             (foldl Tapp (Tcon (mn,c))
 181                                (map (Tvar . fst) utbs)) ts) tbs
 182     ch _ = cenv
 183
 184 mkTypeEnvs :: [Tdef] -> CheckResult (Tcenv, Cenv)
 185 mkTypeEnvs tdefs = do
 186   tcenv <- foldM checkTdef0 eempty tdefs
 187   cenv <- foldM (checkTdef tcenv) eempty tdefs
 188   return (tcenv, cenv)
 189
 190 mkTypeEnvsNoChecking :: [Tdef] -> (Tcenv, Cenv)
 191 mkTypeEnvsNoChecking tdefs =
 192   let tcenv = foldl processTdef0NoChecking eempty tdefs
 193       cenv  = foldl processCdef eempty tdefs in
 194     (tcenv, cenv)
 195
 196 requireModulesEq :: Show a => Mname -> AnMname -> String -> a
 197                           -> Bool -> CheckResult ()
 198 requireModulesEq (Just mn) m msg t _      = require (mn == m) (mkErrMsg msg t)
 199 requireModulesEq Nothing _ msg t emptyOk  = require emptyOk (mkErrMsg msg t)
 200
 201 mkErrMsg :: Show a => String -> a -> String
 202 mkErrMsg msg t = "wrong module name in " ++ msg ++ ":\n" ++ show t
 203
 204 checkVdefg :: Bool -> (Tcenv,Tvenv,Cenv) -> (Venv,Venv)
 205                -> Vdefg -> CheckResult (Venv,Venv)
 206 checkVdefg top_level (tcenv,tvenv,cenv) (e_venv,l_venv) vdefg = do
 207       mn <- getMname
 208       case vdefg of
 209         Rec vdefs ->
 210             do (e_venv', l_venv') <- makeEnv mn vdefs
 211                let env' = (tcenv,tvenv,cenv,e_venv',l_venv')
 212                mapM_ (checkVdef (\ vdef k -> require (k `eqKind` Klifted)
 213                         ("unlifted kind in:\n" ++ show vdef)) env')
 214                      vdefs
 215                return (e_venv', l_venv')
 216         Nonrec vdef ->
 217             do let env' = (tcenv, tvenv, cenv, e_venv, l_venv)
 218                checkVdef (\ vdef k -> do
 219                      require (not (k `eqKind` Kopen)) ("open kind in:\n" ++ show vdef)
 220                      require ((not top_level) || (not (k `eqKind` Kunlifted)))
 221                        ("top-level unlifted kind in:\n" ++ show vdef)) env' vdef
 222                makeEnv mn [vdef]
 223
 224   where makeEnv mn vdefs = do
 225              ev <- foldM (extendVenv False) e_venv e_vts
 226              lv <- foldM (extendVenv False) l_venv l_vts
 227              return (ev, lv)
 228            where e_vts = [ (v,t) | Vdef ((Just m,v),t,_) <- vdefs,
 229                                      not (vdefIsMainWrapper mn (Just m))]
 230                  l_vts = [ (v,t) | Vdef ((Nothing,v),t,_) <- vdefs]
 231         checkVdef checkKind env (vdef@(Vdef ((m,_),t,e))) = do
 232           mn <- getMname
 233           let isZcMain = vdefIsMainWrapper mn m
 234           unless isZcMain $
 235              requireModulesEq m mn "value definition" vdef True
 236           k <- checkTy (tcenv,tvenv) t
 237           checkKind vdef k
 238           t' <- checkExp env e
 239           require (t == t')
 240                    ("declared type doesn't match expression type in:\n"
 241                     ++ show vdef ++ "\n" ++
 242                     "declared type: " ++ show t ++ "\n" ++
 243                     "expression type: " ++ show t')
 244
 245 vdefIsMainWrapper :: AnMname -> Mname -> Bool
 246 vdefIsMainWrapper enclosing defining =
 247    enclosing == mainMname && defining == wrapperMainAnMname
 248
 249 checkExpr :: AnMname -> Menv -> Tcenv -> Cenv -> Venv -> Tvenv
 250                -> Exp -> Ty
 251 checkExpr mn menv _tcenv _cenv venv tvenv e = case runReaderT (do
 252   --(tcenv, cenv) <- mkTypeEnvs tdefs
 253   -- Since the preprocessor calls checkExpr after code has been
 254   -- typechecked, we expect to find the external env in the Menv.
 255   case (elookup menv mn) of
 256      Just thisEnv ->
 257        checkExp ({-tcenv-}tcenv_ thisEnv, tvenv, {-cenv-}cenv_ thisEnv, (venv_ thisEnv), venv) e
 258      Nothing -> reportError e ("checkExpr: Environment for " ++
 259                   show mn ++ " not found")) (mn,menv) of
 260          OkC t -> t
 261          FailC s -> reportError e s
 262
 263 checkType :: AnMname -> Menv -> Tcenv -> Tvenv -> Ty -> Kind
 264 checkType mn menv _tcenv tvenv t =
 265  case runReaderT (checkTy (tcenv_ (fromMaybe (error "checkType") (elookup menv mn)), tvenv) t) (mn, menv) of
 266       OkC k -> k
 267       FailC s -> reportError tvenv (s ++ "\n " ++ show menv ++ "\n mname =" ++ show mn)
 268
 269 checkExp :: (Tcenv,Tvenv,Cenv,Venv,Venv) -> Exp -> CheckResult Ty
 270 checkExp (tcenv,tvenv,cenv,e_venv,l_venv) = ch
 271       where
 272         ch e0 =
 273           case e0 of
 274             Var qv ->
 275               qlookupM venv_ e_venv l_venv qv
 276             Dcon qc ->
 277               qlookupM cenv_ cenv eempty qc
 278             Lit l ->
 279               checkLit l
 280             Appt e t ->
 281               do t' <- ch e
 282                  k' <- checkTy (tcenv,tvenv) t
 283                  case t' of
 284                    Tforall (tv,k) t0 ->
 285                      do require (k' `subKindOf` k)
 286                                 ("kind doesn't match at type application in:\n" ++ show e0 ++ "\n" ++
 287                                  "operator kind: " ++ show k ++ "\n" ++
 288                                  "operand kind: " ++ show k')
 289                         return (substl [tv] [t] t0)
 290                    _ -> fail ("bad operator type in type application:\n" ++ show e0 ++ "\n" ++
 291                                "operator type: " ++ show t')
 292             App e1 e2 ->
 293               do t1 <- ch e1
 294                  t2 <- ch e2
 295                  case t1 of
 296                    Tapp(Tapp(Tcon tc) t') t0 | tc == tcArrow ->
 297                         do require (t2 == t')
 298                                     ("type doesn't match at application in:\n" ++ show e0 ++ "\n" ++
 299                                      "operator type: " ++ show t' ++ "\n" ++
 300                                      "operand type: " ++ show t2)
 301                            return t0
 302                    _ -> fail ("bad operator type at application in:\n" ++ show e0 ++ "\n" ++
 303                                "operator type: " ++ show t1)
 304             Lam (Tb tb) e ->
 305               do tvenv' <- extendTvenv tvenv tb
 306                  t <- checkExp (tcenv,tvenv',cenv,e_venv,l_venv) e
 307                  return (Tforall tb t)
 308             Lam (Vb (vb@(_,vt))) e ->
 309               do k <- checkTy (tcenv,tvenv) vt
 310                  require (baseKind k)
 311                          ("higher-order kind in:\n" ++ show e0 ++ "\n" ++
 312                           "kind: " ++ show k)
 313                  l_venv' <- extendVenv True l_venv vb
 314                  t <- checkExp (tcenv,tvenv,cenv,e_venv,l_venv') e
 315                  require (not (isUtupleTy vt)) ("lambda-bound unboxed tuple in:\n" ++ show e0)
 316                  return (tArrow vt t)
 317             Let vdefg e ->
 318               do (e_venv',l_venv') <- checkVdefg False (tcenv,tvenv,cenv)
 319                                         (e_venv,l_venv) vdefg
 320                  checkExp (tcenv,tvenv,cenv,e_venv',l_venv') e
 321             Case e (v,t) resultTy alts ->
 322               do t' <- ch e
 323                  checkTy (tcenv,tvenv) t
 324                  require (t == t')
 325                           ("scrutinee declared type doesn't match expression type in:\n" ++ show e0 ++ "\n" ++
 326                            "declared type: " ++ show t ++ "\n" ++
 327                            "expression type: " ++ show t')
 328                  case (reverse alts) of
 329                    (Acon c _ _ _):as ->
 330                       let ok ((Acon c _ _ _):as) cs = do require (notElem c cs)
 331                                                                  ("duplicate alternative in case:\n" ++ show e0)
 332                                                          ok as (c:cs)
 333                           ok ((Alit _ _):_)      _  = fail ("invalid alternative in constructor case:\n" ++ show e0)
 334                           ok [Adefault _]        _  = return ()
 335                           ok (Adefault _:_)      _  = fail ("misplaced default alternative in case:\n" ++ show e0)
 336                           ok []                  _  = return ()
 337                       in ok as [c]
 338                    (Alit l _):as ->
 339                       let ok ((Acon _ _ _ _):_) _  = fail ("invalid alternative in literal case:\n" ++ show e0)
 340                           ok ((Alit l _):as)    ls = do require (notElem l ls)
 341                                                                 ("duplicate alternative in case:\n" ++ show e0)
 342                                                         ok as (l:ls)
 343                           ok [Adefault _]       _  = return ()
 344                           ok (Adefault _:_)     _  = fail ("misplaced default alternative in case:\n" ++ show e0)
 345                           ok []                 _  = fail ("missing default alternative in literal case:\n" ++ show e0)
 346                       in ok as [l]
 347                    [Adefault _] -> return ()
 348                    _ -> fail ("no alternatives in case:\n" ++ show e0)
 349                  l_venv' <- extendVenv True l_venv (v,t)
 350                  t:ts <- mapM (checkAlt (tcenv,tvenv,cenv,e_venv,l_venv') t) alts
 351                  require (all (== t) ts)
 352                          ("alternative types don't match in:\n" ++ show e0 ++ "\n" ++
 353                           "types: " ++ show (t:ts))
 354                  checkTy (tcenv,tvenv) resultTy
 355                  require (t == resultTy) ("case alternative type doesn't " ++
 356                    " match case return type in:\n" ++ show e0 ++ "\n" ++
 357                    "alt type: " ++ show t ++ " return type: " ++ show resultTy)
 358                  return t
 359             c@(Cast e t) ->
 360               do eTy <- ch e
 361                  (fromTy, toTy) <- checkTyCo (tcenv,tvenv) t
 362                  require (eTy == fromTy) ("Type mismatch in cast: c = "
 363                              ++ show c ++ "\nand eTy = " ++ show eTy
 364                              ++ "\n and " ++ show fromTy)
 365                  return toTy
 366             Note _ e ->
 367               ch e
 368             External _ t ->
 369               do checkTy (tcenv,eempty) t {- external types must be closed -}
 370                  return t
 371
 372 checkAlt :: (Tcenv,Tvenv,Cenv,Venv,Venv) -> Ty -> Alt -> CheckResult Ty
 373 checkAlt (env@(tcenv,tvenv,cenv,e_venv,l_venv)) t0 = ch
 374       where
 375         ch a0 =
 376           case a0 of
 377             Acon qc etbs vbs e ->
 378               do let uts = f t0
 379                        where f (Tapp t0 t) = f t0 ++ [t]
 380                              f _ = []
 381                  ct <- qlookupM cenv_ cenv eempty qc
 382                  let (tbs,ct_args0,ct_res0) = splitTy ct
 383                  {- get universals -}
 384                  let (utbs,etbs') = splitAt (length uts) tbs
 385                  let utvs = map fst utbs
 386                  {- check existentials -}
 387                  let (etvs,eks) = unzip etbs
 388                  let (etvs',eks') = unzip etbs'
 389                  require (all (uncurry eqKind)
 390                             (zip eks eks'))
 391                          ("existential kinds don't match in:\n" ++ show a0 ++ "\n" ++
 392                           "kinds declared in data constructor: " ++ show eks ++
 393                           "kinds declared in case alternative: " ++ show eks')
 394                  tvenv' <- foldM extendTvenv tvenv etbs
 395                  {- check term variables -}
 396                  let vts = map snd vbs
 397                  mapM_ (\vt -> require ((not . isUtupleTy) vt)
 398                                        ("pattern-bound unboxed tuple in:\n" ++ show a0 ++ "\n" ++
 399                                         "pattern type: " ++ show vt)) vts
 400                  vks <- mapM (checkTy (tcenv,tvenv')) vts
 401                  mapM_ (\vk -> require (baseKind vk)
 402                                        ("higher-order kind in:\n" ++ show a0 ++ "\n" ++
 403                                         "kind: " ++ show vk)) vks
 404                  let (ct_res:ct_args) = map (substl (utvs++etvs') (uts++(map Tvar etvs))) (ct_res0:ct_args0)
 405                  zipWithM_
 406                     (\ct_arg vt ->
 407                         require (ct_arg == vt)
 408                                  ("pattern variable type doesn't match constructor argument type in:\n" ++ show a0 ++ "\n" ++
 409                                   "pattern variable type: " ++ show ct_arg ++ "\n" ++
 410                                   "constructor argument type: " ++ show vt)) ct_args vts
 411                  require (ct_res == t0)
 412                           ("pattern constructor type doesn't match scrutinee type in:\n" ++ show a0 ++ "\n" ++
 413                            "pattern constructor type: " ++ show ct_res ++ "\n" ++
 414                            "scrutinee type: " ++ show t0)
 415                  l_venv' <- foldM (extendVenv True) l_venv vbs
 416                  t <- checkExp (tcenv,tvenv',cenv,e_venv,l_venv') e
 417                  checkTy (tcenv,tvenv) t  {- check that existentials don't escape in result type -}
 418                  return t
 419             Alit l e ->
 420               do t <- checkLit l
 421                  require (t == t0)
 422                          ("pattern type doesn't match scrutinee type in:\n" ++ show a0 ++ "\n" ++
 423                           "pattern type: " ++ show t ++ "\n" ++
 424                           "scrutinee type: " ++ show t0)
 425                  checkExp env e
 426             Adefault e ->
 427               checkExp env e
 428
 429 checkTy :: (Tcenv,Tvenv) -> Ty -> CheckResult Kind
 430 checkTy es@(tcenv,tvenv) = ch
 431      where
 432        ch (Tvar tv) = do
 433           res <- lookupM tvenv tv
 434           case res of
 435             Just k  -> return k
 436             Nothing -> fail ("Undefined tvar: " ++ show tv)
 437        ch (Tcon qtc) = do
 438          kOrC <- qlookupM tcenv_ tcenv eempty qtc
 439          case kOrC of
 440             Kind k -> return k
 441             Coercion (DefinedCoercion [] (t1,t2)) -> return $ Keq t1 t2
 442             Coercion _ -> fail ("Unsaturated coercion app: " ++ show qtc)
 443        ch (t@(Tapp t1 t2)) =
 444              case splitTyConApp_maybe t of
 445                Just (tc, tys) -> do
 446                  tcK <- qlookupM tcenv_ tcenv eempty tc
 447                  case tcK of
 448                    Kind _ -> checkTapp t1 t2
 449                    Coercion co@(DefinedCoercion tbs _) -> do
 450                      -- makes sure coercion is fully applied
 451                      require (length tys == length tbs) $
 452                         ("Arity mismatch in coercion app: " ++ show t)
 453                      let (_, tks) = unzip tbs
 454                      argKs <- mapM (checkTy es) tys
 455                      let kPairs = zip argKs tks
 456                          -- Simon says it's okay for these to be
 457                          -- subkinds
 458                      let kindsOk = all (uncurry subKindOf) kPairs
 459                      require kindsOk
 460                         ("Kind mismatch in coercion app: " ++ show tks
 461                          ++ " and " ++ show argKs ++ " t = " ++ show t)
 462                      return $ (uncurry Keq) (applyNewtype co tys)
 463                Nothing -> checkTapp t1 t2
 464             where checkTapp t1 t2 = do
 465                     k1 <- ch t1
 466                     k2 <- ch t2
 467                     case k1 of
 468                       Karrow k11 k12 -> do
 469                          require (k2 `subKindOf` k11) kindError
 470                          return k12
 471                             where kindError =
 472                                     "kinds don't match in type application: "
 473                                     ++ show t ++ "\n" ++
 474                                     "operator kind: " ++ show k11 ++ "\n" ++
 475                                     "operand kind: " ++ show k2
 476                       _ -> fail ("applied type has non-arrow kind: " ++ show t)
 477
 478        ch (Tforall tb t) =
 479             do tvenv' <- extendTvenv tvenv tb
 480                checkTy (tcenv,tvenv') t
 481        ch (TransCoercion t1 t2) = do
 482             (ty1,ty2) <- checkTyCo es t1
 483             (ty3,ty4) <- checkTyCo es t2
 484             require (ty2 == ty3) ("Types don't match in trans. coercion: " ++
 485                         show ty2 ++ " and " ++ show ty3)
 486             return $ Keq ty1 ty4
 487        ch (SymCoercion t1) = do
 488             (ty1,ty2) <- checkTyCo es t1
 489             return $ Keq ty2 ty1
 490        ch (UnsafeCoercion t1 t2) = do
 491             checkTy es t1
 492             checkTy es t2
 493             return $ Keq t1 t2
 494        ch (LeftCoercion t1) = do
 495             k <- checkTyCo es t1
 496             case k of
 497               ((Tapp u _), (Tapp w _)) -> return $ Keq u w
 498               _ -> fail ("Bad coercion kind in operand of left: " ++ show k)
 499        ch (RightCoercion t1) = do
 500             k <- checkTyCo es t1
 501             case k of
 502               ((Tapp _ v), (Tapp _ x)) -> return $ Keq v x
 503               _ -> fail ("Bad coercion kind in operand of left: " ++ show k)
 504        ch (InstCoercion ty arg) = do
 505             forallK <- checkTyCo es ty
 506             case forallK of
 507               ((Tforall (v1,k1) b1), (Tforall (v2,k2) b2)) -> do
 508                  require (k1 `eqKind` k2) ("Kind mismatch in argument of inst: "
 509                                             ++ show ty)
 510                  argK <- checkTy es arg
 511                  require (argK `eqKind` k1) ("Kind mismatch in type being "
 512                            ++ "instantiated: " ++ show arg)
 513                  let newLhs = substl [v1] [arg] b1
 514                  let newRhs = substl [v2] [arg] b2
 515                  return $ Keq newLhs newRhs
 516               _ -> fail ("Non-forall-ty in argument to inst: " ++ show ty)
 517
 518 checkTyCo :: (Tcenv, Tvenv) -> Ty -> CheckResult (Ty, Ty)
 519 checkTyCo es@(tcenv,_) t@(Tapp t1 t2) =
 520   (case splitTyConApp_maybe t of
 521     Just (tc, tys) -> do
 522        tcK <- qlookupM tcenv_ tcenv eempty tc
 523        case tcK of
 524  -- todo: avoid duplicating this code
 525  -- blah, this almost calls for a different syntactic form
 526  -- (for a defined-coercion app): (TCoercionApp Tcon [Ty])
 527          Coercion co@(DefinedCoercion tbs _) -> do
 528            require (length tys == length tbs) $
 529             ("Arity mismatch in coercion app: " ++ show t)
 530            let (_, tks) = unzip tbs
 531            argKs <- mapM (checkTy es) tys
 532            let kPairs = zip argKs tks
 533            let kindsOk = all (uncurry subKindOf) kPairs
 534            require kindsOk
 535               ("Kind mismatch in coercion app: " ++ show tks
 536                  ++ " and " ++ show argKs ++ " t = " ++ show t)
 537            return (applyNewtype co tys)
 538          _ -> checkTapp t1 t2
 539     _ -> checkTapp t1 t2)
 540        where checkTapp t1 t2 = do
 541                (lhsRator, rhsRator) <- checkTyCo es t1
 542                (lhs, rhs) <- checkTyCo es t2
 543                -- Comp rule from paper
 544                checkTy es (Tapp lhsRator lhs)
 545                checkTy es (Tapp rhsRator rhs)
 546                return (Tapp lhsRator lhs, Tapp rhsRator rhs)
 547 checkTyCo (tcenv, tvenv) (Tforall tb t) = do
 548   tvenv' <- extendTvenv tvenv tb
 549   (t1,t2) <- checkTyCo (tcenv, tvenv') t
 550   return (Tforall tb t1, Tforall tb t2)
 551 checkTyCo es t = do
 552   k <- checkTy es t
 553   case k of
 554     Keq t1 t2 -> return (t1, t2)
 555     -- otherwise, expand by the "refl" rule
 556     _          -> return (t, t)
 557
 558 mlookupM :: (Eq a, Show a, Show b) => (Envs -> Env a b) -> Env a b -> Env a b -> Mname
 559           -> CheckResult (Env a b)
 560 mlookupM _ _ local_env    Nothing            = -- (trace ("mlookupM_: returning " ++ show local_env)) $
 561   return local_env
 562 mlookupM selector external_env local_env (Just m) = do
 563   mn <- getMname
 564   globalEnv <- getGlobalEnv
 565   if m == mn
 566      then -- trace ("global env would b e " ++ show (elookup globalEnv m)) $
 567             return external_env
 568      else
 569        case elookup globalEnv m of
 570          Just env' -> return (selector env')
 571          Nothing -> fail ("Check: undefined module name: "
 572                       ++ show m ++ show (edomain local_env))
 573
 574 qlookupM :: (Ord a, Show a,Show b) => (Envs -> Env a b) -> Env a b -> Env a b
 575                   -> Qual a -> CheckResult b
 576 qlookupM selector external_env local_env v@(m,k) =
 577       do env <- -- trace ("qlookupM: " ++ show v) $
 578                   mlookupM selector external_env local_env m
 579          -- argh, hack for unqualified top-level names
 580          maybeRes <- lookupM env k
 581          case maybeRes of
 582            Just r -> return r
 583            Nothing -> do mn <- getMname
 584                          currentMenv <- --  trace ("qlookupM: trying module for " ++ show mn) $
 585                                          mlookupM selector external_env local_env (Just mn)
 586                          maybeRes1 <- -- trace ("qlookupM: trying in " ++ show currentMenv) $
 587                                         lookupM currentMenv k
 588                          case maybeRes1 of
 589                            Just r1 -> return r1
 590                            Nothing -> do
 591                              globalEnv <- getGlobalEnv
 592                              case elookup globalEnv mn of
 593                                Just e1 -> case elookup (selector e1) k of
 594                                             Just r2 -> return r2
 595                                             Nothing -> fail ("Undefined id " ++ show v)
 596                                Nothing -> fail ("Undefined id " ++ show v)
 597
 598 checkLit :: Lit -> CheckResult Ty
 599 checkLit (Literal lit t) =
 600   case lit of
 601     Lint _ ->
 602           do require (t `elem` intLitTypes)
 603                      ("invalid int literal: " ++ show lit ++ "\n" ++ "type: " ++ show t)
 604              return t
 605     Lrational _ ->
 606           do require (t `elem` ratLitTypes)
 607                      ("invalid rational literal: " ++ show lit ++ "\n" ++ "type: " ++ show t)
 608              return t
 609     Lchar _ ->
 610           do require (t `elem` charLitTypes)
 611                      ("invalid char literal: " ++ show lit ++ "\n" ++ "type: " ++ show t)
 612              return t
 613     Lstring _ ->
 614           do require (t `elem` stringLitTypes)
 615                      ("invalid string literal: " ++ show lit ++ "\n" ++ "type: " ++ show t)
 616              return t
 617
 618 {- Utilities -}
 619
 620 {- Split off tbs, arguments and result of a (possibly abstracted)  arrow type -}
 621 splitTy :: Ty -> ([Tbind],[Ty],Ty)
 622 splitTy (Tforall tb t) = (tb:tbs,ts,tr)
 623                 where (tbs,ts,tr) = splitTy t
 624 splitTy (Tapp(Tapp(Tcon tc) t0) t) | tc == tcArrow = (tbs,t0:ts,tr)
 625                 where (tbs,ts,tr) = splitTy t
 626 splitTy t = ([],[],t)
 627
 628
 629 primCoercionError :: Show a => a -> b
 630 primCoercionError s = error $ "Bad coercion application: " ++ show s
 631
 632 -- todo
 633 reportError :: Show a => a -> String -> b
 634 reportError e s = error $ ("Core type error: checkExpr failed with "
 635                    ++ s ++ " and " ++ show e)
 636
 637 type NtEnv  = M.Map Tcon CoercionKind
 638
 639 mkNtEnv :: Menv -> NtEnv
 640 mkNtEnv menv =
 641   foldl M.union M.empty $
 642         map (\ (_,e) ->
 643                  foldr (\ (_,thing) rest ->
 644                             case thing of
 645                               Kind _ -> rest
 646                               Coercion d@(DefinedCoercion _ (lhs,_)) ->
 647                                   case splitTyConApp_maybe lhs of
 648                                     Just ((_,tc1),_) -> M.insert tc1 d rest
 649                                     _ -> rest) M.empty (etolist (tcenv_ e))) (etolist menv)