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