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