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