ghc/compiler/typecheck/TcArrows.lhs

   1 %
   2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
   3 %
   4 \section{Typecheck arrow notation}
   5
   6 \begin{code}
   7 module TcArrows ( tcProc ) where
   8
   9 #include "HsVersions.h"
  10
  11 import {-# SOURCE #-}   TcExpr( tcCheckRho )
  12
  13 import HsSyn
  14 import TcHsSyn  ( TcCmd, TcCmdTop, TcExpr, TcPat, mkHsLet )
  15
  16 import TcMatches ( TcStmtCtxt(..), tcMatchPats, matchCtxt, tcStmts )
  17
  18 import TcType   ( TcType, TcTauType, TcRhoType, mkFunTys, mkTyConApp,
  19                   mkTyVarTy, mkAppTys, tcSplitTyConApp_maybe, tcEqType )
  20 import TcMType  ( newTyVar, newTyVarTy, newTyVarTys, newSigTyVar, zonkTcType )
  21 import TcBinds  ( tcBindsAndThen )
  22 import TcSimplify ( tcSimplifyCheck )
  23 import TcUnify  ( Expected(..), checkSigTyVarsWrt, zapExpectedTo )
  24 import TcRnMonad
  25 import Inst     ( tcSyntaxName )
  26 import TysWiredIn ( boolTy, pairTyCon )
  27 import VarSet
  28 import Type     ( Kind,
  29                   mkArrowKinds, liftedTypeKind, openTypeKind, tyVarsOfTypes )
  30 import RnHsSyn  ( RenamedHsExpr, RenamedPat, RenamedHsCmd, RenamedHsCmdTop )
  31
  32 import Outputable
  33 import Util     ( lengthAtLeast )
  34
  35 \end{code}
  36
  37 %************************************************************************
  38 %*                                                                      *
  39                 Proc
  40 %*                                                                      *
  41 %************************************************************************
  42
  43 \begin{code}
  44 tcProc :: RenamedPat -> RenamedHsCmdTop         -- proc pat -> expr
  45        -> Expected TcRhoType                    -- Expected type of whole proc expression
  46        -> TcM (TcPat, TcCmdTop)
  47
  48 tcProc pat cmd exp_ty
  49  = do   { arr_ty <- newTyVarTy arrowTyConKind
  50         ; [arg_ty, res_ty] <- newTyVarTys 2 liftedTypeKind
  51         ; zapExpectedTo exp_ty (mkAppTys arr_ty [arg_ty,res_ty])
  52
  53         ; let cmd_env = CmdEnv { cmd_arr = arr_ty }
  54         ; ([pat'], cmd', ex_binds) <- incProcLevel $
  55                                       tcMatchPats [(pat, Check arg_ty)] (Check res_ty) $
  56                                       tcCmdTop cmd_env cmd ([], res_ty)
  57
  58         ; return (pat', glueBindsOnCmd ex_binds cmd') }
  59 \end{code}
  60
  61
  62 %************************************************************************
  63 %*                                                                      *
  64                 Commands
  65 %*                                                                      *
  66 %************************************************************************
  67
  68 \begin{code}
  69 type CmdStack = [TcTauType]
  70 data CmdEnv   = CmdEnv { cmd_arr   :: TcType }          -- The arrow type constructor, of kind *->*->*
  71
  72 mkCmdArrTy :: CmdEnv -> TcTauType -> TcTauType -> TcTauType
  73 mkCmdArrTy env t1 t2 = mkAppTys (cmd_arr env) [t1, t2]
  74
  75 ---------------------------------------
  76 tcCmdTop :: CmdEnv
  77         -> RenamedHsCmdTop
  78         -> (CmdStack, TcTauType)        -- Expected result type; always a monotype
  79                                         -- We know exactly how many cmd args are expected,
  80                                         -- albeit perhaps not their types; so we can pass
  81                                         -- in a CmdStack
  82         -> TcM TcCmdTop
  83
  84 tcCmdTop env (HsCmdTop cmd _ _ names) (cmd_stk, res_ty)
  85   = do  { cmd'   <- tcCmd env cmd (cmd_stk, res_ty)
  86         ; names' <- mapM (tcSyntaxName ProcOrigin (cmd_arr env)) names
  87         ; return (HsCmdTop cmd' cmd_stk res_ty names') }
  88
  89
  90 ----------------------------------------
  91 tcCmd :: CmdEnv -> RenamedHsExpr -> (CmdStack, TcTauType) -> TcM TcExpr
  92         -- The main recursive function
  93
  94 tcCmd env (HsPar cmd) res_ty
  95   = do  { cmd' <- tcCmd env cmd res_ty
  96         ; return (HsPar cmd') }
  97
  98 tcCmd env (HsLet binds body) res_ty
  99   = tcBindsAndThen HsLet binds $
 100     tcCmd env body res_ty
 101
 102 tcCmd env (HsIf pred b1 b2 src_loc) res_ty
 103   = addSrcLoc src_loc   $
 104     do  { pred' <- tcCheckRho pred boolTy
 105         ; b1'   <- tcCmd env b1 res_ty
 106         ; b2'   <- tcCmd env b2 res_ty
 107         ; return (HsIf pred' b1' b2' src_loc)
 108     }
 109
 110 -------------------------------------------
 111 --              Arrow application
 112 --          (f -< a)   or   (f =< a)
 113
 114 tcCmd env cmd@(HsArrApp fun arg _ ho_app lr src_loc) (cmd_stk, res_ty)
 115   = addSrcLoc src_loc           $
 116     addErrCtxt (cmdCtxt cmd)    $
 117     do  { arg_ty <- newTyVarTy openTypeKind
 118         ; let fun_ty = mkCmdArrTy env arg_ty res_ty
 119
 120         ; checkTc (null cmd_stk) (nonEmptyCmdStkErr cmd)
 121
 122         ; fun' <- pop_arrow_binders (tcCheckRho fun fun_ty)
 123
 124         ; arg' <- tcCheckRho arg arg_ty
 125
 126         ; return (HsArrApp fun' arg' fun_ty ho_app lr src_loc) }
 127   where
 128         -- Before type-checking f, remove the "arrow binders" from the
 129         -- environment in the (-<) case.
 130         -- Local bindings, inside the enclosing proc, are not in scope
 131         -- inside f.  In the higher-order case (--<), they are.
 132     pop_arrow_binders tc = case ho_app of
 133         HsHigherOrderApp -> tc
 134         HsFirstOrderApp  -> popArrowBinders tc
 135
 136 -------------------------------------------
 137 --              Command application
 138
 139 tcCmd env cmd@(HsApp fun arg) (cmd_stk, res_ty)
 140   = addErrCtxt (cmdCtxt cmd)    $
 141     do  { arg_ty <- newTyVarTy openTypeKind
 142
 143         ; fun' <- tcCmd env fun (arg_ty:cmd_stk, res_ty)
 144
 145         ; arg' <- tcCheckRho arg arg_ty
 146
 147         ; return (HsApp fun' arg') }
 148
 149 -------------------------------------------
 150 --              Lambda
 151
 152 tcCmd env cmd@(HsLam match@(Match pats maybe_rhs_sig grhss)) (cmd_stk, res_ty)
 153   = addSrcLoc (getMatchLoc match)               $
 154     addErrCtxt (matchCtxt match_ctxt match)     $
 155
 156     do  {       -- Check the cmd stack is big enough
 157         ; checkTc (lengthAtLeast cmd_stk n_pats)
 158                   (kappaUnderflow cmd)
 159         ; let pats_w_tys = zip pats (map Check cmd_stk)
 160
 161                 -- Check the patterns, and the GRHSs inside
 162         ; (pats', grhss', ex_binds) <- tcMatchPats pats_w_tys (Check res_ty) $
 163                                        tc_grhss grhss
 164
 165         ; return (HsLam (Match pats' Nothing (glueBindsOnGRHSs ex_binds grhss')))
 166         }
 167
 168   where
 169     n_pats     = length pats
 170     stk'       = drop n_pats cmd_stk
 171     match_ctxt = LambdaExpr     -- Maybe KappaExpr?
 172
 173     tc_grhss (GRHSs grhss binds _)
 174         = tcBindsAndThen glueBindsOnGRHSs binds         $
 175           do { grhss' <- mappM tc_grhs grhss
 176              ; return (GRHSs grhss' EmptyBinds res_ty) }
 177
 178     stmt_ctxt = SC { sc_what = PatGuard match_ctxt,
 179                      sc_rhs  = tcCheckRho,
 180                      sc_body = \ body -> tcCmd env body (stk', res_ty),
 181                      sc_ty   = res_ty } -- ToDo: Is this right?
 182     tc_grhs (GRHS guarded locn)
 183         = addSrcLoc locn        $
 184           do { guarded' <- tcStmts stmt_ctxt guarded
 185              ; return (GRHS guarded' locn) }
 186
 187 -------------------------------------------
 188 --              Do notation
 189
 190 tcCmd env cmd@(HsDo do_or_lc stmts _ ty src_loc) (cmd_stk, res_ty)
 191   = do  { checkTc (null cmd_stk) (nonEmptyCmdStkErr cmd)
 192         ; stmts' <- tcStmts stmt_ctxt stmts
 193         ; return (HsDo do_or_lc stmts' [] res_ty src_loc) }
 194         -- The 'methods' needed for the HsDo are in the enclosing HsCmd
 195         -- hence the empty list here
 196   where
 197     stmt_ctxt = SC { sc_what = do_or_lc,
 198                      sc_rhs  = tc_rhs,
 199                      sc_body = tc_ret,
 200                      sc_ty   = res_ty }
 201
 202     tc_rhs rhs ty = tcCmd env rhs  ([], ty)
 203     tc_ret body   = tcCmd env body ([], res_ty)
 204
 205
 206 -----------------------------------------------------------------
 207 --      Arrow ``forms''       (| e |) c1 .. cn
 208 --
 209 --      G      |-b  c : [s1 .. sm] s
 210 --      pop(G) |-   e : forall w. b ((w,s1) .. sm) s
 211 --                              -> a ((w,t1) .. tn) t
 212 --      e \not\in (s, s1..sm, t, t1..tn)
 213 --      ----------------------------------------------
 214 --      G |-a  (| e |) c  :  [t1 .. tn] t
 215
 216 tcCmd env cmd@(HsArrForm expr fixity cmd_args src_loc) (cmd_stk, res_ty)
 217   = addSrcLoc src_loc           $
 218     addErrCtxt (cmdCtxt cmd)    $
 219     do  { cmds_w_tys <- mapM new_cmd_ty (cmd_args `zip` [1..])
 220         ; w_tv       <- newSigTyVar liftedTypeKind
 221         ; let w_ty = mkTyVarTy w_tv
 222
 223                 --  a ((w,t1) .. tn) t
 224         ; let e_res_ty = mkCmdArrTy env (foldl mkPairTy w_ty cmd_stk) res_ty
 225
 226                 --   b ((w,s1) .. sm) s
 227                 --   -> a ((w,t1) .. tn) t
 228         ; let e_ty = mkFunTys [mkAppTys b [tup,s] | (_,_,b,tup,s) <- cmds_w_tys]
 229                               e_res_ty
 230
 231                 -- Check expr
 232         ; (expr', lie) <- getLIE (tcCheckRho expr e_ty)
 233         ; inst_binds <- tcSimplifyCheck sig_msg [w_tv] [] lie
 234
 235                 -- Check that the polymorphic variable hasn't been unified with anything
 236                 -- and is not free in res_ty or the cmd_stk  (i.e.  t, t1..tn)
 237         ; [w_tv'] <- checkSigTyVarsWrt (tyVarsOfTypes (res_ty:cmd_stk))
 238                                        [w_tv]
 239
 240                 -- OK, now we are in a position to unscramble
 241                 -- the s1..sm and check each cmd
 242         ; cmds' <- mapM (tc_cmd w_tv') cmds_w_tys
 243
 244         ; returnM (HsArrForm (TyLam [w_tv'] (mkHsLet inst_binds expr')) fixity cmds' src_loc)
 245         }
 246   where
 247         -- Make the types
 248         --      b, ((e,s1) .. sm), s
 249     new_cmd_ty :: (RenamedHsCmdTop, Int)
 250                -> TcM (RenamedHsCmdTop, Int, TcType, TcType, TcType)
 251     new_cmd_ty (cmd,i)
 252           = do  { b_ty   <- newTyVarTy arrowTyConKind
 253                 ; tup_ty <- newTyVarTy liftedTypeKind
 254                         -- We actually make a type variable for the tuple
 255                         -- because we don't know how deeply nested it is yet
 256                 ; s_ty   <- newTyVarTy liftedTypeKind
 257                 ; return (cmd, i, b_ty, tup_ty, s_ty)
 258                 }
 259
 260     tc_cmd w_tv (cmd, i, b, tup_ty, s)
 261       = do { tup_ty' <- zonkTcType tup_ty
 262            ; let (corner_ty, arg_tys) = unscramble tup_ty'
 263
 264                 -- Check that it has the right shape:
 265                 --      ((w,s1) .. sn)
 266                 -- where the si do not mention w
 267            ; checkTc (corner_ty `tcEqType` mkTyVarTy w_tv &&
 268                       not (w_tv `elemVarSet` tyVarsOfTypes arg_tys))
 269                      (badFormFun i tup_ty')
 270
 271            ; tcCmdTop (CmdEnv { cmd_arr = b }) cmd (arg_tys, s) }
 272
 273     unscramble :: TcType -> (TcType, [TcType])
 274     -- unscramble ((w,s1) .. sn)        =  (w, [s1..sn])
 275     unscramble ty
 276        = case tcSplitTyConApp_maybe ty of
 277             Just (tc, [t,s]) | tc == pairTyCon
 278                ->  let
 279                       (w,ss) = unscramble t
 280                    in (w, s:ss)
 281
 282             other -> (ty, [])
 283
 284     sig_msg  = ptext SLIT("expected type of a command form")
 285
 286 -----------------------------------------------------------------
 287 --              Base case for illegal commands
 288 -- This is where expressions that aren't commands get rejected
 289
 290 tcCmd env cmd _
 291   = failWithTc (vcat [ptext SLIT("The expression"), nest 2 (ppr cmd),
 292                       ptext SLIT("was found where an arrow command was expected")])
 293 \end{code}
 294
 295
 296 %************************************************************************
 297 %*                                                                      *
 298                 Helpers
 299 %*                                                                      *
 300 %************************************************************************
 301
 302
 303 \begin{code}
 304 glueBindsOnCmd EmptyBinds cmd                             = cmd
 305 glueBindsOnCmd binds      (HsCmdTop cmd stk res_ty names) = HsCmdTop (HsLet binds cmd) stk res_ty names
 306         -- Existential bindings become local bindings in the command
 307
 308
 309 mkPairTy t1 t2 = mkTyConApp pairTyCon [t1,t2]
 310
 311 arrowTyConKind :: Kind          -- *->*->*
 312 arrowTyConKind = mkArrowKinds [liftedTypeKind, liftedTypeKind] liftedTypeKind
 313 \end{code}
 314
 315
 316 %************************************************************************
 317 %*                                                                      *
 318                 Errors
 319 %*                                                                      *
 320 %************************************************************************
 321
 322 \begin{code}
 323 cmdCtxt cmd = ptext SLIT("In the command:") <+> ppr cmd
 324
 325 nonEmptyCmdStkErr cmd
 326   = hang (ptext SLIT("Non-empty command stack at command:"))
 327          4 (ppr cmd)
 328
 329 kappaUnderflow cmd
 330   = hang (ptext SLIT("Command stack underflow at command:"))
 331          4 (ppr cmd)
 332
 333 badFormFun i tup_ty'
 334  = hang (ptext SLIT("The type of the") <+> speakNth i <+> ptext SLIT("argument of a command form has the wrong shape"))
 335         4 (ptext SLIT("Argument type:") <+> ppr tup_ty')
 336 \end{code}