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