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 -------------------------------------------
 138 --              Lambda
 139
 140 tcCmd env cmd@(HsLam match@(Match pats maybe_rhs_sig grhss)) (cmd_stk, res_ty)
 141   = addSrcLoc (getMatchLoc match)               $
 142     addErrCtxt (matchCtxt match_ctxt match)     $
 143
 144     do  {       -- Check the cmd stack is big enough
 145         ; checkTc (lengthAtLeast cmd_stk n_pats)
 146                   (kappaUnderflow cmd)
 147         ; let pats_w_tys = zip pats (map Check cmd_stk)
 148
 149                 -- Check the patterns, and the GRHSs inside
 150         ; (pats', grhss', ex_binds) <- tcMatchPats pats_w_tys (Check res_ty) $
 151                                        tc_grhss grhss
 152
 153         ; return (HsLam (Match pats' Nothing (glueBindsOnGRHSs ex_binds grhss')))
 154         }
 155
 156   where
 157     n_pats     = length pats
 158     stk'       = drop n_pats cmd_stk
 159     match_ctxt = LambdaExpr     -- Maybe KappaExpr?
 160
 161     tc_grhss (GRHSs grhss binds _)
 162         = tcBindsAndThen glueBindsOnGRHSs binds         $
 163           do { grhss' <- mappM tc_grhs grhss
 164              ; return (GRHSs grhss' EmptyBinds res_ty) }
 165
 166     stmt_ctxt = SC { sc_what = PatGuard match_ctxt,
 167                      sc_rhs  = tcCheckRho,
 168                      sc_body = \ body -> tcCmd env body (stk', res_ty),
 169                      sc_ty   = res_ty } -- ToDo: Is this right?
 170     tc_grhs (GRHS guarded locn)
 171         = addSrcLoc locn        $
 172           do { guarded' <- tcStmts stmt_ctxt guarded
 173              ; return (GRHS guarded' locn) }
 174
 175 -------------------------------------------
 176 --              Do notation
 177
 178 tcCmd env cmd@(HsDo do_or_lc stmts _ ty src_loc) (cmd_stk, res_ty)
 179   = do  { checkTc (null cmd_stk) (nonEmptyCmdStkErr cmd)
 180         ; stmts' <- tcStmts stmt_ctxt stmts
 181         ; return (HsDo do_or_lc stmts' [] res_ty src_loc) }
 182         -- The 'methods' needed for the HsDo are in the enclosing HsCmd
 183         -- hence the empty list here
 184   where
 185     stmt_ctxt = SC { sc_what = do_or_lc,
 186                      sc_rhs  = tc_rhs,
 187                      sc_body = tc_ret,
 188                      sc_ty   = res_ty }
 189
 190     tc_rhs rhs ty = tcCmd env rhs  ([], ty)
 191     tc_ret body   = tcCmd env body ([], res_ty)
 192
 193
 194 -----------------------------------------------------------------
 195 --      Arrow ``forms''       (| e |) c1 .. cn
 196 --
 197 --      G      |-b  c : [s1 .. sm] s
 198 --      pop(G) |-   e : forall w. b ((w,s1) .. sm) s
 199 --                              -> a ((w,t1) .. tn) t
 200 --      e \not\in (s, s1..sm, t, t1..tn)
 201 --      ----------------------------------------------
 202 --      G |-a  (| e |) c  :  [t1 .. tn] t
 203
 204 tcCmd env cmd@(HsArrForm expr fixity cmd_args src_loc) (cmd_stk, res_ty)
 205   = addSrcLoc src_loc           $
 206     addErrCtxt (cmdCtxt cmd)    $
 207     do  { cmds_w_tys <- mapM new_cmd_ty (cmd_args `zip` [1..])
 208         ; w_tv       <- newSigTyVar liftedTypeKind
 209         ; let w_ty = mkTyVarTy w_tv
 210
 211                 --  a ((w,t1) .. tn) t
 212         ; let e_res_ty = mkCmdArrTy env (foldl mkPairTy w_ty cmd_stk) res_ty
 213
 214                 --   b ((w,s1) .. sm) s
 215                 --   -> a ((w,t1) .. tn) t
 216         ; let e_ty = mkFunTys [mkAppTys b [tup,s] | (_,_,b,tup,s) <- cmds_w_tys]
 217                               e_res_ty
 218
 219                 -- Check expr
 220         ; (expr', lie) <- getLIE (tcCheckRho expr e_ty)
 221         ; inst_binds <- tcSimplifyCheck sig_msg [w_tv] [] lie
 222
 223                 -- Check that the polymorphic variable hasn't been unified with anything
 224                 -- and is not free in res_ty or the cmd_stk  (i.e.  t, t1..tn)
 225         ; [w_tv'] <- checkSigTyVarsWrt (tyVarsOfTypes (res_ty:cmd_stk))
 226                                        [w_tv]
 227
 228                 -- OK, now we are in a position to unscramble
 229                 -- the s1..sm and check each cmd
 230         ; cmds' <- mapM (tc_cmd w_tv') cmds_w_tys
 231
 232         ; returnM (HsArrForm (TyLam [w_tv'] (mkHsLet inst_binds expr')) fixity cmds' src_loc)
 233         }
 234   where
 235         -- Make the types
 236         --      b, ((e,s1) .. sm), s
 237     new_cmd_ty :: (RenamedHsCmdTop, Int)
 238                -> TcM (RenamedHsCmdTop, Int, TcType, TcType, TcType)
 239     new_cmd_ty (cmd,i)
 240           = do  { b_ty   <- newTyVarTy arrowTyConKind
 241                 ; tup_ty <- newTyVarTy liftedTypeKind
 242                         -- We actually make a type variable for the tuple
 243                         -- because we don't know how deeply nested it is yet
 244                 ; s_ty   <- newTyVarTy liftedTypeKind
 245                 ; return (cmd, i, b_ty, tup_ty, s_ty)
 246                 }
 247
 248     tc_cmd w_tv (cmd, i, b, tup_ty, s)
 249       = do { tup_ty' <- zonkTcType tup_ty
 250            ; let (corner_ty, arg_tys) = unscramble tup_ty'
 251
 252                 -- Check that it has the right shape:
 253                 --      ((w,s1) .. sn)
 254                 -- where the si do not mention w
 255            ; checkTc (corner_ty `tcEqType` mkTyVarTy w_tv &&
 256                       not (w_tv `elemVarSet` tyVarsOfTypes arg_tys))
 257                      (badFormFun i tup_ty')
 258
 259            ; tcCmdTop (CmdEnv { cmd_arr = b }) cmd (arg_tys, s) }
 260
 261     unscramble :: TcType -> (TcType, [TcType])
 262     -- unscramble ((w,s1) .. sn)        =  (w, [s1..sn])
 263     unscramble ty
 264        = case tcSplitTyConApp_maybe ty of
 265             Just (tc, [t,s]) | tc == pairTyCon
 266                ->  let
 267                       (w,ss) = unscramble t
 268                    in (w, s:ss)
 269
 270             other -> (ty, [])
 271
 272     sig_msg  = ptext SLIT("expected type of a command form")
 273
 274 -----------------------------------------------------------------
 275 --              Base case for illegal commands
 276 -- This is where expressions that aren't commands get rejected
 277
 278 tcCmd env cmd _
 279   = failWithTc (vcat [ptext SLIT("The expression"), nest 2 (ppr cmd),
 280                       ptext SLIT("was found where an arrow command was expected")])
 281 \end{code}
 282
 283
 284 %************************************************************************
 285 %*                                                                      *
 286                 Helpers
 287 %*                                                                      *
 288 %************************************************************************
 289
 290
 291 \begin{code}
 292 glueBindsOnCmd EmptyBinds cmd                             = cmd
 293 glueBindsOnCmd binds      (HsCmdTop cmd stk res_ty names) = HsCmdTop (HsLet binds cmd) stk res_ty names
 294         -- Existential bindings become local bindings in the command
 295
 296
 297 mkPairTy t1 t2 = mkTyConApp pairTyCon [t1,t2]
 298
 299 arrowTyConKind :: Kind          -- *->*->*
 300 arrowTyConKind = mkArrowKinds [liftedTypeKind, liftedTypeKind] liftedTypeKind
 301 \end{code}
 302
 303
 304 %************************************************************************
 305 %*                                                                      *
 306                 Errors
 307 %*                                                                      *
 308 %************************************************************************
 309
 310 \begin{code}
 311 cmdCtxt cmd = ptext SLIT("In the command:") <+> ppr cmd
 312
 313 nonEmptyCmdStkErr cmd
 314   = hang (ptext SLIT("Non-empty command stack at command:"))
 315          4 (ppr cmd)
 316
 317 kappaUnderflow cmd
 318   = hang (ptext SLIT("Command stack underflow at command:"))
 319          4 (ppr cmd)
 320
 321 badFormFun i tup_ty'
 322  = hang (ptext SLIT("The type of the") <+> speakNth i <+> ptext SLIT("argument of a command form has the wrong shape"))
 323         4 (ptext SLIT("Argument type:") <+> ppr tup_ty')
 324 \end{code}