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