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