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