compiler/typecheck/TcArrows.lhs

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