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