Merge branch 'master' into type-nats
[ghc.git] / 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 -fno-warn-tabs #-}
9 -- The above warning supression flag is a temporary kludge.
10 -- While working on this module you are encouraged to remove it and
11 -- detab the module (please do the detabbing in a separate patch). See
12 --     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#TabsvsSpaces
13 -- for details
14
15 module TcArrows ( tcProc ) where
16
17 import {-# SOURCE #-}   TcExpr( tcMonoExpr, tcInferRho, tcSyntaxOp, tcCheckId )
18
19 import HsSyn
20 import TcMatches
21 import TcType
22 import TcMType
23 import TcBinds
24 import TcPat
25 import TcUnify
26 import TcRnMonad
27 import TcEnv
28 import TcEvidence
29 import Id( mkLocalId )
30 import Inst
31 import Name
32 import TysWiredIn
33 import VarSet 
34 import TysPrim
35
36 import SrcLoc
37 import Outputable
38 import FastString
39 import Util
40
41 import Control.Monad
42 \end{code}
43
44 %************************************************************************
45 %*                                                                      *
46                 Proc    
47 %*                                                                      *
48 %************************************************************************
49
50 \begin{code}
51 tcProc :: InPat Name -> LHsCmdTop Name          -- proc pat -> expr
52        -> TcRhoType                             -- Expected type of whole proc expression
53        -> TcM (OutPat TcId, LHsCmdTop TcId, TcCoercion)
54
55 tcProc pat cmd exp_ty
56   = newArrowScope $
57     do  { (co, (exp_ty1, res_ty)) <- matchExpectedAppTy exp_ty 
58         ; (co1, (arr_ty, arg_ty)) <- matchExpectedAppTy exp_ty1
59         ; let cmd_env = CmdEnv { cmd_arr = arr_ty }
60         ; (pat', cmd') <- tcPat ProcExpr pat arg_ty $
61                           tcCmdTop cmd_env cmd [] res_ty
62         ; let res_co = mkTcTransCo co (mkTcAppCo co1 (mkTcReflCo res_ty))
63         ; return (pat', cmd', res_co) }
64 \end{code}
65
66
67 %************************************************************************
68 %*                                                                      *
69                 Commands
70 %*                                                                      *
71 %************************************************************************
72
73 \begin{code}
74 type CmdStack = [TcTauType]
75 data CmdEnv
76   = CmdEnv {
77         cmd_arr         :: TcType -- arrow type constructor, of kind *->*->*
78     }
79
80 mkCmdArrTy :: CmdEnv -> TcTauType -> TcTauType -> TcTauType
81 mkCmdArrTy env t1 t2 = mkAppTys (cmd_arr env) [t1, t2]
82
83 ---------------------------------------
84 tcCmdTop :: CmdEnv 
85          -> LHsCmdTop Name
86          -> CmdStack
87          -> TcTauType   -- Expected result type; always a monotype
88                              -- We know exactly how many cmd args are expected,
89                              -- albeit perhaps not their types; so we can pass 
90                              -- in a CmdStack
91         -> TcM (LHsCmdTop TcId)
92
93 tcCmdTop env (L loc (HsCmdTop cmd _ _ names)) cmd_stk res_ty
94   = setSrcSpan loc $
95     do  { cmd'   <- tcCmd env cmd (cmd_stk, res_ty)
96         ; names' <- mapM (tcSyntaxName ProcOrigin (cmd_arr env)) names
97         ; return (L loc $ HsCmdTop cmd' cmd_stk res_ty names') }
98
99
100 ----------------------------------------
101 tcCmd :: CmdEnv -> LHsExpr Name -> (CmdStack, TcTauType) -> TcM (LHsExpr TcId)
102         -- The main recursive function
103 tcCmd env (L loc expr) res_ty
104   = setSrcSpan loc $ do
105         { expr' <- tc_cmd env expr res_ty
106         ; return (L loc expr') }
107
108 tc_cmd :: CmdEnv -> HsExpr Name -> (CmdStack, TcTauType) -> TcM (HsExpr TcId)
109 tc_cmd env (HsPar cmd) res_ty
110   = do  { cmd' <- tcCmd env cmd res_ty
111         ; return (HsPar cmd') }
112
113 tc_cmd env (HsLet binds (L body_loc body)) res_ty
114   = do  { (binds', body') <- tcLocalBinds binds         $
115                              setSrcSpan body_loc        $
116                              tc_cmd env body res_ty
117         ; return (HsLet binds' (L body_loc body')) }
118
119 tc_cmd env in_cmd@(HsCase scrut matches) (stk, res_ty)
120   = addErrCtxt (cmdCtxt in_cmd) $ do
121       (scrut', scrut_ty) <- tcInferRho scrut 
122       matches' <- tcMatchesCase match_ctxt scrut_ty matches res_ty
123       return (HsCase scrut' matches')
124   where
125     match_ctxt = MC { mc_what = CaseAlt,
126                       mc_body = mc_body }
127     mc_body body res_ty' = tcCmd env body (stk, res_ty')
128
129 tc_cmd env (HsIf Nothing pred b1 b2) res_ty    -- Ordinary 'if'
130   = do  { pred' <- tcMonoExpr pred boolTy
131         ; b1'   <- tcCmd env b1 res_ty
132         ; b2'   <- tcCmd env b2 res_ty
133         ; return (HsIf Nothing pred' b1' b2')
134     }
135
136 tc_cmd env (HsIf (Just fun) pred b1 b2) res_ty -- Rebindable syntax for if
137   = do  { pred_ty <- newFlexiTyVarTy openTypeKind
138         -- For arrows, need ifThenElse :: forall r. T -> r -> r -> r
139         -- because we're going to apply it to the environment, not
140         -- the return value.
141         ; [r_tv] <- tcInstSkolTyVars [alphaTyVar]
142         ; let r_ty = mkTyVarTy r_tv
143         ; let if_ty = mkFunTys [pred_ty, r_ty, r_ty] r_ty
144         ; checkTc (not (r_tv `elemVarSet` tyVarsOfType pred_ty))
145                   (ptext (sLit "Predicate type of `ifThenElse' depends on result type"))
146         ; fun'  <- tcSyntaxOp IfOrigin fun if_ty
147         ; pred' <- tcMonoExpr pred pred_ty
148         ; b1'   <- tcCmd env b1 res_ty
149         ; b2'   <- tcCmd env b2 res_ty
150         ; return (HsIf (Just fun') pred' b1' b2')
151     }
152
153 -------------------------------------------
154 --              Arrow application
155 --          (f -< a)   or   (f -<< a)
156
157 tc_cmd env cmd@(HsArrApp fun arg _ ho_app lr) (cmd_stk, res_ty)
158   = addErrCtxt (cmdCtxt cmd)    $
159     do  { arg_ty <- newFlexiTyVarTy openTypeKind
160         ; let fun_ty = mkCmdArrTy env (foldl mkPairTy arg_ty cmd_stk) res_ty
161
162         ; fun' <- select_arrow_scope (tcMonoExpr fun fun_ty)
163
164         ; arg' <- tcMonoExpr arg arg_ty
165
166         ; return (HsArrApp fun' arg' fun_ty ho_app lr) }
167   where
168         -- Before type-checking f, use the environment of the enclosing
169         -- proc for the (-<) case.  
170         -- Local bindings, inside the enclosing proc, are not in scope 
171         -- inside f.  In the higher-order case (-<<), they are.
172     select_arrow_scope tc = case ho_app of
173         HsHigherOrderApp -> tc
174         HsFirstOrderApp  -> escapeArrowScope tc
175
176 -------------------------------------------
177 --              Command application
178
179 tc_cmd env cmd@(HsApp fun arg) (cmd_stk, res_ty)
180   = addErrCtxt (cmdCtxt cmd)    $
181     do  { arg_ty <- newFlexiTyVarTy openTypeKind
182
183         ; fun' <- tcCmd env fun (arg_ty:cmd_stk, res_ty)
184
185         ; arg' <- tcMonoExpr arg arg_ty
186
187         ; return (HsApp fun' arg') }
188
189 -------------------------------------------
190 --              Lambda
191
192 tc_cmd env cmd@(HsLam (MatchGroup [L mtch_loc (match@(Match pats _maybe_rhs_sig grhss))] _))
193        (cmd_stk, res_ty)
194   = addErrCtxt (pprMatchInCtxt match_ctxt match)        $
195
196     do  {       -- Check the cmd stack is big enough
197         ; checkTc (lengthAtLeast cmd_stk n_pats)
198                   (kappaUnderflow cmd)
199
200                 -- Check the patterns, and the GRHSs inside
201         ; (pats', grhss') <- setSrcSpan mtch_loc                $
202                              tcPats LambdaExpr pats cmd_stk     $
203                              tc_grhss grhss res_ty
204
205         ; let match' = L mtch_loc (Match pats' Nothing grhss')
206         ; return (HsLam (MatchGroup [match'] res_ty))
207         }
208
209   where
210     n_pats     = length pats
211     stk'       = drop n_pats cmd_stk
212     match_ctxt = (LambdaExpr :: HsMatchContext Name)    -- Maybe KappaExpr?
213     pg_ctxt    = PatGuard match_ctxt
214
215     tc_grhss (GRHSs grhss binds) res_ty
216         = do { (binds', grhss') <- tcLocalBinds binds $
217                                    mapM (wrapLocM (tc_grhs res_ty)) grhss
218              ; return (GRHSs grhss' binds') }
219
220     tc_grhs res_ty (GRHS guards body)
221         = do { (guards', rhs') <- tcStmtsAndThen pg_ctxt tcGuardStmt guards res_ty $
222                                   \ res_ty -> tcCmd env body (stk', res_ty)
223              ; return (GRHS guards' rhs') }
224
225 -------------------------------------------
226 --              Do notation
227
228 tc_cmd env cmd@(HsDo do_or_lc stmts _) (cmd_stk, res_ty)
229   = do  { checkTc (null cmd_stk) (nonEmptyCmdStkErr cmd)
230         ; stmts' <- tcStmts do_or_lc (tcArrDoStmt env) stmts res_ty 
231         ; return (HsDo do_or_lc stmts' res_ty) }
232   where
233
234
235 -----------------------------------------------------------------
236 --      Arrow ``forms''       (| e c1 .. cn |)
237 --
238 --      G      |-b  c : [s1 .. sm] s
239 --      pop(G) |-   e : forall w. b ((w,s1) .. sm) s
240 --                              -> a ((w,t1) .. tn) t
241 --      e \not\in (s, s1..sm, t, t1..tn)
242 --      ----------------------------------------------
243 --      G |-a  (| e c |)  :  [t1 .. tn] t
244
245 tc_cmd env cmd@(HsArrForm expr fixity cmd_args) (cmd_stk, res_ty)       
246   = addErrCtxt (cmdCtxt cmd)    $
247     do  { cmds_w_tys <- zipWithM new_cmd_ty cmd_args [1..]
248         ; [w_tv]     <- tcInstSkolTyVars [alphaTyVar]
249         ; let w_ty = mkTyVarTy w_tv     -- Just a convenient starting point
250
251                 --  a ((w,t1) .. tn) t
252         ; let e_res_ty = mkCmdArrTy env (foldl mkPairTy w_ty cmd_stk) res_ty
253
254                 --   b ((w,s1) .. sm) s
255                 --   -> a ((w,t1) .. tn) t
256         ; let e_ty = mkFunTys [mkAppTys b [tup,s] | (_,_,b,tup,s) <- cmds_w_tys] 
257                               e_res_ty
258
259                 -- Check expr
260         ; (inst_binds, expr') <- checkConstraints ArrowSkol [w_tv] [] $
261                                  escapeArrowScope (tcMonoExpr expr e_ty)
262
263                 -- OK, now we are in a position to unscramble 
264                 -- the s1..sm and check each cmd
265         ; cmds' <- mapM (tc_cmd w_tv) cmds_w_tys
266
267         ; let wrap = WpTyLam w_tv <.> mkWpLet inst_binds
268         ; return (HsArrForm (mkLHsWrap wrap expr') fixity cmds') }
269   where
270         -- Make the types       
271         --      b, ((e,s1) .. sm), s
272     new_cmd_ty :: LHsCmdTop Name -> Int
273                -> TcM (LHsCmdTop Name, Int, TcType, TcType, TcType)
274     new_cmd_ty cmd i
275           = do  { b_ty   <- newFlexiTyVarTy arrowTyConKind
276                 ; tup_ty <- newFlexiTyVarTy liftedTypeKind
277                         -- We actually make a type variable for the tuple
278                         -- because we don't know how deeply nested it is yet    
279                 ; s_ty   <- newFlexiTyVarTy liftedTypeKind
280                 ; return (cmd, i, b_ty, tup_ty, s_ty)
281                 }
282
283     tc_cmd w_tv (cmd, i, b, tup_ty, s)
284       = do { tup_ty' <- zonkTcType tup_ty
285            ; let (corner_ty, arg_tys) = unscramble tup_ty'
286
287                 -- Check that it has the right shape:
288                 --      ((w,s1) .. sn)
289                 -- where the si do not mention w
290            ; _bogus <- unifyType corner_ty (mkTyVarTy w_tv)
291            ; checkTc (not (w_tv `elemVarSet` tyVarsOfTypes arg_tys))
292                      (badFormFun i tup_ty')
293      -- JPM: WARNING: this test is utterly bogus; see #5609
294      -- We are not using the coercion returned by the unify;
295      -- and (even more seriously) the w not in arg_tys test is totally
296      -- bogus if there are suspended equality constraints. This code
297      -- needs to be re-architected.
298
299            ; tcCmdTop (env { cmd_arr = b }) cmd arg_tys s }
300
301     unscramble :: TcType -> (TcType, [TcType])
302     -- unscramble ((w,s1) .. sn)        =  (w, [s1..sn])
303     unscramble ty = unscramble' ty []
304
305     unscramble' ty ss
306        = case tcSplitTyConApp_maybe ty of
307             Just (tc, [t,s]) | tc == pairTyCon 
308                ->  unscramble' t (s:ss)
309             _ -> (ty, ss)
310
311 -----------------------------------------------------------------
312 --              Base case for illegal commands
313 -- This is where expressions that aren't commands get rejected
314
315 tc_cmd _ cmd _
316   = failWithTc (vcat [ptext (sLit "The expression"), nest 2 (ppr cmd), 
317                       ptext (sLit "was found where an arrow command was expected")])
318 \end{code}
319
320
321 %************************************************************************
322 %*                                                                      *
323                 Stmts
324 %*                                                                      *
325 %************************************************************************
326
327 \begin{code}
328 --------------------------------
329 --      Mdo-notation
330 -- The distinctive features here are
331 --      (a) RecStmts, and
332 --      (b) no rebindable syntax
333
334 tcArrDoStmt :: CmdEnv -> TcStmtChecker
335 tcArrDoStmt env _ (LastStmt rhs _) res_ty thing_inside
336   = do  { rhs' <- tcCmd env rhs ([], res_ty)
337         ; thing <- thing_inside (panic "tcArrDoStmt")
338         ; return (LastStmt rhs' noSyntaxExpr, thing) }
339
340 tcArrDoStmt env _ (ExprStmt rhs _ _ _) res_ty thing_inside
341   = do  { (rhs', elt_ty) <- tc_arr_rhs env rhs
342         ; thing          <- thing_inside res_ty
343         ; return (ExprStmt rhs' noSyntaxExpr noSyntaxExpr elt_ty, thing) }
344
345 tcArrDoStmt env ctxt (BindStmt pat rhs _ _) res_ty thing_inside
346   = do  { (rhs', pat_ty) <- tc_arr_rhs env rhs
347         ; (pat', thing)  <- tcPat (StmtCtxt ctxt) pat pat_ty $
348                             thing_inside res_ty
349         ; return (BindStmt pat' rhs' noSyntaxExpr noSyntaxExpr, thing) }
350
351 tcArrDoStmt env ctxt (RecStmt { recS_stmts = stmts, recS_later_ids = later_names
352                             , recS_rec_ids = rec_names }) res_ty thing_inside
353   = do  { let tup_names = rec_names ++ filterOut (`elem` rec_names) later_names
354         ; tup_elt_tys <- newFlexiTyVarTys (length tup_names) liftedTypeKind
355         ; let tup_ids = zipWith mkLocalId tup_names tup_elt_tys
356         ; tcExtendIdEnv tup_ids $ do
357         { (stmts', tup_rets)
358                 <- tcStmtsAndThen ctxt (tcArrDoStmt env) stmts res_ty   $ \ _res_ty' ->
359                         -- ToDo: res_ty not really right
360                    zipWithM tcCheckId tup_names tup_elt_tys
361
362         ; thing <- thing_inside res_ty
363                 -- NB:  The rec_ids for the recursive things 
364                 --      already scope over this part. This binding may shadow
365                 --      some of them with polymorphic things with the same Name
366                 --      (see note [RecStmt] in HsExpr)
367
368         ; let rec_ids = takeList rec_names tup_ids
369         ; later_ids <- tcLookupLocalIds later_names
370
371         ; let rec_rets = takeList rec_names tup_rets
372         ; let ret_table = zip tup_ids tup_rets
373         ; let later_rets = [r | i <- later_ids, (j, r) <- ret_table, i == j]
374
375         ; return (emptyRecStmt { recS_stmts = stmts', recS_later_ids = later_ids
376                                , recS_later_rets = later_rets
377                                , recS_rec_ids = rec_ids, recS_rec_rets = rec_rets
378                                , recS_ret_ty = res_ty }, thing)
379         }}
380
381 tcArrDoStmt _ _ stmt _ _
382   = pprPanic "tcArrDoStmt: unexpected Stmt" (ppr stmt)
383
384 tc_arr_rhs :: CmdEnv -> LHsExpr Name -> TcM (LHsExpr TcId, TcType)
385 tc_arr_rhs env rhs = do { ty <- newFlexiTyVarTy liftedTypeKind
386                         ; rhs' <- tcCmd env rhs ([], ty)
387                         ; return (rhs', ty) }
388 \end{code}
389
390
391 %************************************************************************
392 %*                                                                      *
393                 Helpers
394 %*                                                                      *
395 %************************************************************************
396
397
398 \begin{code}
399 mkPairTy :: Type -> Type -> Type
400 mkPairTy t1 t2 = mkTyConApp pairTyCon [t1,t2]
401
402 arrowTyConKind :: Kind          --  *->*->*
403 arrowTyConKind = mkArrowKinds [liftedTypeKind, liftedTypeKind] liftedTypeKind
404 \end{code}
405
406
407 %************************************************************************
408 %*                                                                      *
409                 Errors
410 %*                                                                      *
411 %************************************************************************
412
413 \begin{code}
414 cmdCtxt :: HsExpr Name -> SDoc
415 cmdCtxt cmd = ptext (sLit "In the command:") <+> ppr cmd
416
417 nonEmptyCmdStkErr :: HsExpr Name -> SDoc
418 nonEmptyCmdStkErr cmd
419   = hang (ptext (sLit "Non-empty command stack at command:"))
420        2 (ppr cmd)
421
422 kappaUnderflow :: HsExpr Name -> SDoc
423 kappaUnderflow cmd
424   = hang (ptext (sLit "Command stack underflow at command:"))
425        2 (ppr cmd)
426
427 badFormFun :: Int -> TcType -> SDoc
428 badFormFun i tup_ty'
429  = hang (ptext (sLit "The type of the") <+> speakNth i <+> ptext (sLit "argument of a command form has the wrong shape"))
430       2 (ptext (sLit "Argument type:") <+> ppr tup_ty')
431 \end{code}