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