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