utils/ext-core/Check.hs

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