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