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