compiler/typecheck/TcArrows.hs

   1 {-
   2 (c) The University of Glasgow 2006
   3 (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
   4
   5 Typecheck arrow notation
   6 -}
   7
   8 {-# LANGUAGE RankNTypes, TupleSections #-}
   9 {-# LANGUAGE TypeFamilies #-}
  10
  11 module TcArrows ( tcProc ) where
  12
  13 import GhcPrelude
  14
  15 import {-# SOURCE #-}   TcExpr( tcMonoExpr, tcInferRho, tcSyntaxOp, tcCheckId, tcPolyExpr )
  16
  17 import GHC.Hs
  18 import TcMatches
  19 import TcHsSyn( hsPatType )
  20 import TcType
  21 import TcMType
  22 import TcBinds
  23 import TcPat
  24 import TcUnify
  25 import TcRnMonad
  26 import TcEnv
  27 import TcEvidence
  28 import Id( mkLocalId )
  29 import Inst
  30 import Name
  31 import TysWiredIn
  32 import VarSet
  33 import TysPrim
  34 import BasicTypes( Arity )
  35 import SrcLoc
  36 import Outputable
  37 import Util
  38
  39 import Control.Monad
  40
  41 {-
  42 Note [Arrow overview]
  43 ~~~~~~~~~~~~~~~~~~~~~
  44 Here's a summary of arrows and how they typecheck.  First, here's
  45 a cut-down syntax:
  46
  47   expr ::= ....
  48         |  proc pat cmd
  49
  50   cmd ::= cmd exp                    -- Arrow application
  51        |  \pat -> cmd                -- Arrow abstraction
  52        |  (| exp cmd1 ... cmdn |)    -- Arrow form, n>=0
  53        |  ... -- If, case in the usual way
  54
  55   cmd_type ::= carg_type --> type
  56
  57   carg_type ::= ()
  58              |  (type, carg_type)
  59
  60 Note that
  61  * The 'exp' in an arrow form can mention only
  62    "arrow-local" variables
  63
  64  * An "arrow-local" variable is bound by an enclosing
  65    cmd binding form (eg arrow abstraction)
  66
  67  * A cmd_type is here written with a funny arrow "-->",
  68    The bit on the left is a carg_type (command argument type)
  69    which itself is a nested tuple, finishing with ()
  70
  71  * The arrow-tail operator (e1 -< e2) means
  72        (| e1 <<< arr snd |) e2
  73
  74
  75 ************************************************************************
  76 *                                                                      *
  77                 Proc
  78 *                                                                      *
  79 ************************************************************************
  80 -}
  81
  82 tcProc :: InPat GhcRn -> LHsCmdTop GhcRn        -- proc pat -> expr
  83        -> ExpRhoType                            -- Expected type of whole proc expression
  84        -> TcM (OutPat GhcTcId, LHsCmdTop GhcTcId, TcCoercion)
  85
  86 tcProc pat cmd exp_ty
  87   = newArrowScope $
  88     do  { exp_ty <- expTypeToType exp_ty  -- no higher-rank stuff with arrows
  89         ; (co, (exp_ty1, res_ty)) <- matchExpectedAppTy exp_ty
  90         ; (co1, (arr_ty, arg_ty)) <- matchExpectedAppTy exp_ty1
  91         ; let cmd_env = CmdEnv { cmd_arr = arr_ty }
  92         ; (pat', cmd') <- tcPat ProcExpr pat (mkCheckExpType arg_ty) $
  93                           tcCmdTop cmd_env cmd (unitTy, res_ty)
  94         ; let res_co = mkTcTransCo co
  95                          (mkTcAppCo co1 (mkTcNomReflCo res_ty))
  96         ; return (pat', cmd', res_co) }
  97
  98 {-
  99 ************************************************************************
 100 *                                                                      *
 101                 Commands
 102 *                                                                      *
 103 ************************************************************************
 104 -}
 105
 106 -- See Note [Arrow overview]
 107 type CmdType    = (CmdArgType, TcTauType)    -- cmd_type
 108 type CmdArgType = TcTauType                  -- carg_type, a nested tuple
 109
 110 data CmdEnv
 111   = CmdEnv {
 112         cmd_arr :: TcType -- arrow type constructor, of kind *->*->*
 113     }
 114
 115 mkCmdArrTy :: CmdEnv -> TcTauType -> TcTauType -> TcTauType
 116 mkCmdArrTy env t1 t2 = mkAppTys (cmd_arr env) [t1, t2]
 117
 118 ---------------------------------------
 119 tcCmdTop :: CmdEnv
 120          -> LHsCmdTop GhcRn
 121          -> CmdType
 122          -> TcM (LHsCmdTop GhcTcId)
 123
 124 tcCmdTop env (L loc (HsCmdTop names cmd)) cmd_ty@(cmd_stk, res_ty)
 125   = setSrcSpan loc $
 126     do  { cmd'   <- tcCmd env cmd cmd_ty
 127         ; names' <- mapM (tcSyntaxName ProcOrigin (cmd_arr env)) names
 128         ; return (L loc $ HsCmdTop (CmdTopTc cmd_stk res_ty names') cmd') }
 129 tcCmdTop _ (L _ (XCmdTop nec)) _ = noExtCon nec
 130
 131 ----------------------------------------
 132 tcCmd  :: CmdEnv -> LHsCmd GhcRn -> CmdType -> TcM (LHsCmd GhcTcId)
 133         -- The main recursive function
 134 tcCmd env (L loc cmd) res_ty
 135   = setSrcSpan loc $ do
 136         { cmd' <- tc_cmd env cmd res_ty
 137         ; return (L loc cmd') }
 138
 139 tc_cmd :: CmdEnv -> HsCmd GhcRn  -> CmdType -> TcM (HsCmd GhcTcId)
 140 tc_cmd env (HsCmdPar x cmd) res_ty
 141   = do  { cmd' <- tcCmd env cmd res_ty
 142         ; return (HsCmdPar x cmd') }
 143
 144 tc_cmd env (HsCmdLet x (L l binds) (L body_loc body)) res_ty
 145   = do  { (binds', body') <- tcLocalBinds binds         $
 146                              setSrcSpan body_loc        $
 147                              tc_cmd env body res_ty
 148         ; return (HsCmdLet x (L l binds') (L body_loc body')) }
 149
 150 tc_cmd env in_cmd@(HsCmdCase x scrut matches) (stk, res_ty)
 151   = addErrCtxt (cmdCtxt in_cmd) $ do
 152       (scrut', scrut_ty) <- tcInferRho scrut
 153       matches' <- tcMatchesCase match_ctxt scrut_ty matches (mkCheckExpType res_ty)
 154       return (HsCmdCase x scrut' matches')
 155   where
 156     match_ctxt = MC { mc_what = CaseAlt,
 157                       mc_body = mc_body }
 158     mc_body body res_ty' = do { res_ty' <- expTypeToType res_ty'
 159                               ; tcCmd env body (stk, res_ty') }
 160
 161 tc_cmd env (HsCmdIf x Nothing pred b1 b2) res_ty    -- Ordinary 'if'
 162   = do  { pred' <- tcMonoExpr pred (mkCheckExpType boolTy)
 163         ; b1'   <- tcCmd env b1 res_ty
 164         ; b2'   <- tcCmd env b2 res_ty
 165         ; return (HsCmdIf x Nothing pred' b1' b2')
 166     }
 167
 168 tc_cmd env (HsCmdIf x (Just fun) pred b1 b2) res_ty -- Rebindable syntax for if
 169   = do  { pred_ty <- newOpenFlexiTyVarTy
 170         -- For arrows, need ifThenElse :: forall r. T -> r -> r -> r
 171         -- because we're going to apply it to the environment, not
 172         -- the return value.
 173         ; (_, [r_tv]) <- tcInstSkolTyVars [alphaTyVar]
 174         ; let r_ty = mkTyVarTy r_tv
 175         ; checkTc (not (r_tv `elemVarSet` tyCoVarsOfType pred_ty))
 176                   (text "Predicate type of `ifThenElse' depends on result type")
 177         ; (pred', fun')
 178             <- tcSyntaxOp IfOrigin fun (map synKnownType [pred_ty, r_ty, r_ty])
 179                                        (mkCheckExpType r_ty) $ \ _ ->
 180                tcMonoExpr pred (mkCheckExpType pred_ty)
 181
 182         ; b1'   <- tcCmd env b1 res_ty
 183         ; b2'   <- tcCmd env b2 res_ty
 184         ; return (HsCmdIf x (Just fun') pred' b1' b2')
 185     }
 186
 187 -------------------------------------------
 188 --              Arrow application
 189 --          (f -< a)   or   (f -<< a)
 190 --
 191 --   D   |- fun :: a t1 t2
 192 --   D,G |- arg :: t1
 193 --  ------------------------
 194 --   D;G |-a  fun -< arg :: stk --> t2
 195 --
 196 --   D,G |- fun :: a t1 t2
 197 --   D,G |- arg :: t1
 198 --  ------------------------
 199 --   D;G |-a  fun -<< arg :: stk --> t2
 200 --
 201 -- (plus -<< requires ArrowApply)
 202
 203 tc_cmd env cmd@(HsCmdArrApp _ fun arg ho_app lr) (_, res_ty)
 204   = addErrCtxt (cmdCtxt cmd)    $
 205     do  { arg_ty <- newOpenFlexiTyVarTy
 206         ; let fun_ty = mkCmdArrTy env arg_ty res_ty
 207         ; fun' <- select_arrow_scope (tcMonoExpr fun (mkCheckExpType fun_ty))
 208
 209         ; arg' <- tcMonoExpr arg (mkCheckExpType arg_ty)
 210
 211         ; return (HsCmdArrApp fun_ty fun' arg' ho_app lr) }
 212   where
 213        -- Before type-checking f, use the environment of the enclosing
 214        -- proc for the (-<) case.
 215        -- Local bindings, inside the enclosing proc, are not in scope
 216        -- inside f.  In the higher-order case (-<<), they are.
 217        -- See Note [Escaping the arrow scope] in TcRnTypes
 218     select_arrow_scope tc = case ho_app of
 219         HsHigherOrderApp -> tc
 220         HsFirstOrderApp  -> escapeArrowScope tc
 221
 222 -------------------------------------------
 223 --              Command application
 224 --
 225 -- D,G |-  exp : t
 226 -- D;G |-a cmd : (t,stk) --> res
 227 -- -----------------------------
 228 -- D;G |-a cmd exp : stk --> res
 229
 230 tc_cmd env cmd@(HsCmdApp x fun arg) (cmd_stk, res_ty)
 231   = addErrCtxt (cmdCtxt cmd)    $
 232     do  { arg_ty <- newOpenFlexiTyVarTy
 233         ; fun'   <- tcCmd env fun (mkPairTy arg_ty cmd_stk, res_ty)
 234         ; arg'   <- tcMonoExpr arg (mkCheckExpType arg_ty)
 235         ; return (HsCmdApp x fun' arg') }
 236
 237 -------------------------------------------
 238 --              Lambda
 239 --
 240 -- D;G,x:t |-a cmd : stk --> res
 241 -- ------------------------------
 242 -- D;G |-a (\x.cmd) : (t,stk) --> res
 243
 244 tc_cmd env
 245        (HsCmdLam x (MG { mg_alts = L l [L mtch_loc
 246                                    (match@(Match { m_pats = pats, m_grhss = grhss }))],
 247                          mg_origin = origin }))
 248        (cmd_stk, res_ty)
 249   = addErrCtxt (pprMatchInCtxt match)        $
 250     do  { (co, arg_tys, cmd_stk') <- matchExpectedCmdArgs n_pats cmd_stk
 251
 252                 -- Check the patterns, and the GRHSs inside
 253         ; (pats', grhss') <- setSrcSpan mtch_loc                                 $
 254                              tcPats LambdaExpr pats (map mkCheckExpType arg_tys) $
 255                              tc_grhss grhss cmd_stk' (mkCheckExpType res_ty)
 256
 257         ; let match' = L mtch_loc (Match { m_ext = noExtField
 258                                          , m_ctxt = LambdaExpr, m_pats = pats'
 259                                          , m_grhss = grhss' })
 260               arg_tys = map hsPatType pats'
 261               cmd' = HsCmdLam x (MG { mg_alts = L l [match']
 262                                     , mg_ext = MatchGroupTc arg_tys res_ty
 263                                     , mg_origin = origin })
 264         ; return (mkHsCmdWrap (mkWpCastN co) cmd') }
 265   where
 266     n_pats     = length pats
 267     match_ctxt = (LambdaExpr :: HsMatchContext Name)    -- Maybe KappaExpr?
 268     pg_ctxt    = PatGuard match_ctxt
 269
 270     tc_grhss (GRHSs x grhss (L l binds)) stk_ty res_ty
 271         = do { (binds', grhss') <- tcLocalBinds binds $
 272                                    mapM (wrapLocM (tc_grhs stk_ty res_ty)) grhss
 273              ; return (GRHSs x grhss' (L l binds')) }
 274     tc_grhss (XGRHSs nec) _ _ = noExtCon nec
 275
 276     tc_grhs stk_ty res_ty (GRHS x guards body)
 277         = do { (guards', rhs') <- tcStmtsAndThen pg_ctxt tcGuardStmt guards res_ty $
 278                                   \ res_ty -> tcCmd env body
 279                                                 (stk_ty, checkingExpType "tc_grhs" res_ty)
 280              ; return (GRHS x guards' rhs') }
 281     tc_grhs _ _ (XGRHS nec) = noExtCon nec
 282
 283 -------------------------------------------
 284 --              Do notation
 285
 286 tc_cmd env (HsCmdDo _ (L l stmts) ) (cmd_stk, res_ty)
 287   = do  { co <- unifyType Nothing unitTy cmd_stk  -- Expecting empty argument stack
 288         ; stmts' <- tcStmts ArrowExpr (tcArrDoStmt env) stmts res_ty
 289         ; return (mkHsCmdWrap (mkWpCastN co) (HsCmdDo res_ty (L l stmts') )) }
 290
 291
 292 -----------------------------------------------------------------
 293 --      Arrow ``forms''       (| e c1 .. cn |)
 294 --
 295 --      D; G |-a1 c1 : stk1 --> r1
 296 --      ...
 297 --      D; G |-an cn : stkn --> rn
 298 --      D |-  e :: forall e. a1 (e, stk1) t1
 299 --                                ...
 300 --                        -> an (e, stkn) tn
 301 --                        -> a  (e, stk) t
 302 --      e \not\in (stk, stk1, ..., stkm, t, t1, ..., tn)
 303 --      ----------------------------------------------
 304 --      D; G |-a  (| e c1 ... cn |)  :  stk --> t
 305
 306 tc_cmd env cmd@(HsCmdArrForm x expr f fixity cmd_args) (cmd_stk, res_ty)
 307   = addErrCtxt (cmdCtxt cmd)    $
 308     do  { (cmd_args', cmd_tys) <- mapAndUnzipM tc_cmd_arg cmd_args
 309                               -- We use alphaTyVar for 'w'
 310         ; let e_ty = mkInvForAllTy alphaTyVar $
 311                      mkVisFunTys cmd_tys $
 312                      mkCmdArrTy env (mkPairTy alphaTy cmd_stk) res_ty
 313         ; expr' <- tcPolyExpr expr e_ty
 314         ; return (HsCmdArrForm x expr' f fixity cmd_args') }
 315
 316   where
 317     tc_cmd_arg :: LHsCmdTop GhcRn -> TcM (LHsCmdTop GhcTcId, TcType)
 318     tc_cmd_arg cmd
 319        = do { arr_ty <- newFlexiTyVarTy arrowTyConKind
 320             ; stk_ty <- newFlexiTyVarTy liftedTypeKind
 321             ; res_ty <- newFlexiTyVarTy liftedTypeKind
 322             ; let env' = env { cmd_arr = arr_ty }
 323             ; cmd' <- tcCmdTop env' cmd (stk_ty, res_ty)
 324             ; return (cmd',  mkCmdArrTy env' (mkPairTy alphaTy stk_ty) res_ty) }
 325
 326 tc_cmd _ (XCmd nec) _ = noExtCon nec
 327
 328 -----------------------------------------------------------------
 329 --              Base case for illegal commands
 330 -- This is where expressions that aren't commands get rejected
 331
 332 tc_cmd _ cmd _
 333   = failWithTc (vcat [text "The expression", nest 2 (ppr cmd),
 334                       text "was found where an arrow command was expected"])
 335
 336
 337 matchExpectedCmdArgs :: Arity -> TcType -> TcM (TcCoercionN, [TcType], TcType)
 338 matchExpectedCmdArgs 0 ty
 339   = return (mkTcNomReflCo ty, [], ty)
 340 matchExpectedCmdArgs n ty
 341   = do { (co1, [ty1, ty2]) <- matchExpectedTyConApp pairTyCon ty
 342        ; (co2, tys, res_ty) <- matchExpectedCmdArgs (n-1) ty2
 343        ; return (mkTcTyConAppCo Nominal pairTyCon [co1, co2], ty1:tys, res_ty) }
 344
 345 {-
 346 ************************************************************************
 347 *                                                                      *
 348                 Stmts
 349 *                                                                      *
 350 ************************************************************************
 351 -}
 352
 353 --------------------------------
 354 --      Mdo-notation
 355 -- The distinctive features here are
 356 --      (a) RecStmts, and
 357 --      (b) no rebindable syntax
 358
 359 tcArrDoStmt :: CmdEnv -> TcCmdStmtChecker
 360 tcArrDoStmt env _ (LastStmt x rhs noret _) res_ty thing_inside
 361   = do  { rhs' <- tcCmd env rhs (unitTy, res_ty)
 362         ; thing <- thing_inside (panic "tcArrDoStmt")
 363         ; return (LastStmt x rhs' noret noSyntaxExpr, thing) }
 364
 365 tcArrDoStmt env _ (BodyStmt _ rhs _ _) res_ty thing_inside
 366   = do  { (rhs', elt_ty) <- tc_arr_rhs env rhs
 367         ; thing          <- thing_inside res_ty
 368         ; return (BodyStmt elt_ty rhs' noSyntaxExpr noSyntaxExpr, thing) }
 369
 370 tcArrDoStmt env ctxt (BindStmt _ pat rhs _ _) res_ty thing_inside
 371   = do  { (rhs', pat_ty) <- tc_arr_rhs env rhs
 372         ; (pat', thing)  <- tcPat (StmtCtxt ctxt) pat (mkCheckExpType pat_ty) $
 373                             thing_inside res_ty
 374         ; return (mkTcBindStmt pat' rhs', thing) }
 375
 376 tcArrDoStmt env ctxt (RecStmt { recS_stmts = stmts, recS_later_ids = later_names
 377                             , recS_rec_ids = rec_names }) res_ty thing_inside
 378   = do  { let tup_names = rec_names ++ filterOut (`elem` rec_names) later_names
 379         ; tup_elt_tys <- newFlexiTyVarTys (length tup_names) liftedTypeKind
 380         ; let tup_ids = zipWith mkLocalId tup_names tup_elt_tys
 381         ; tcExtendIdEnv tup_ids $ do
 382         { (stmts', tup_rets)
 383                 <- tcStmtsAndThen ctxt (tcArrDoStmt env) stmts res_ty   $ \ _res_ty' ->
 384                         -- ToDo: res_ty not really right
 385                    zipWithM tcCheckId tup_names (map mkCheckExpType tup_elt_tys)
 386
 387         ; thing <- thing_inside res_ty
 388                 -- NB:  The rec_ids for the recursive things
 389                 --      already scope over this part. This binding may shadow
 390                 --      some of them with polymorphic things with the same Name
 391                 --      (see note [RecStmt] in GHC.Hs.Expr)
 392
 393         ; let rec_ids = takeList rec_names tup_ids
 394         ; later_ids <- tcLookupLocalIds later_names
 395
 396         ; let rec_rets = takeList rec_names tup_rets
 397         ; let ret_table = zip tup_ids tup_rets
 398         ; let later_rets = [r | i <- later_ids, (j, r) <- ret_table, i == j]
 399
 400         ; return (emptyRecStmtId { recS_stmts = stmts'
 401                                  , recS_later_ids = later_ids
 402                                  , recS_rec_ids = rec_ids
 403                                  , recS_ext = unitRecStmtTc
 404                                      { recS_later_rets = later_rets
 405                                      , recS_rec_rets = rec_rets
 406                                      , recS_ret_ty = res_ty} }, thing)
 407         }}
 408
 409 tcArrDoStmt _ _ stmt _ _
 410   = pprPanic "tcArrDoStmt: unexpected Stmt" (ppr stmt)
 411
 412 tc_arr_rhs :: CmdEnv -> LHsCmd GhcRn -> TcM (LHsCmd GhcTcId, TcType)
 413 tc_arr_rhs env rhs = do { ty <- newFlexiTyVarTy liftedTypeKind
 414                         ; rhs' <- tcCmd env rhs (unitTy, ty)
 415                         ; return (rhs', ty) }
 416
 417 {-
 418 ************************************************************************
 419 *                                                                      *
 420                 Helpers
 421 *                                                                      *
 422 ************************************************************************
 423 -}
 424
 425 mkPairTy :: Type -> Type -> Type
 426 mkPairTy t1 t2 = mkTyConApp pairTyCon [t1,t2]
 427
 428 arrowTyConKind :: Kind          --  *->*->*
 429 arrowTyConKind = mkVisFunTys [liftedTypeKind, liftedTypeKind] liftedTypeKind
 430
 431 {-
 432 ************************************************************************
 433 *                                                                      *
 434                 Errors
 435 *                                                                      *
 436 ************************************************************************
 437 -}
 438
 439 cmdCtxt :: HsCmd GhcRn -> SDoc
 440 cmdCtxt cmd = text "In the command:" <+> ppr cmd