Some comments and false starts to do with ArrForm
[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 -> LHsExpr Name -> (CmdStack, TcTauType) -> TcM (LHsExpr TcId)
103         -- The main recursive function
104 tcCmd env (L loc expr) res_ty
105   = setSrcSpan loc $ do
106         { expr' <- tc_cmd env expr res_ty
107         ; return (L loc expr') }
108
109 tc_cmd :: CmdEnv -> HsExpr Name -> (CmdStack, TcTauType) -> TcM (HsExpr TcId)
110 tc_cmd env (HsPar cmd) res_ty
111   = do  { cmd' <- tcCmd env cmd res_ty
112         ; return (HsPar cmd') }
113
114 tc_cmd env (HsLet 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 (HsLet binds' (L body_loc body')) }
119
120 tc_cmd env in_cmd@(HsCase 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 (HsCase 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 (HsIf 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 (HsIf Nothing pred' b1' b2')
135     }
136
137 tc_cmd env (HsIf (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 (HsIf (Just fun') pred' b1' b2')
152     }
153
154 -------------------------------------------
155 --              Arrow application
156 --          (f -< a)   or   (f -<< a)
157
158 tc_cmd env cmd@(HsArrApp 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 (HsArrApp 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@(HsApp 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 (HsApp fun' arg') }
191
192 -------------------------------------------
193 --              Lambda
194
195 tc_cmd env cmd@(HsLam (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 (HsLam (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@(HsDo do_or_lc stmts _) (cmd_stk, res_ty)
232   = do  { checkTc (null cmd_stk) (nonEmptyCmdStkErr cmd)
233         ; stmts' <- tcStmts do_or_lc (tcArrDoStmt env) stmts res_ty 
234         ; return (HsDo do_or_lc 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@(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         ; (_, [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 = {- mkWpLet (EvBinds outer_binds) <.> -}
289                      WpTyLam w_tv <.> mkWpLet inner_binds
290         ; return (HsArrForm (mkLHsWrap wrap expr') fixity cmds') }
291   where
292         -- Make the types       
293         --      b, ((e,s1) .. sm), s
294     new_cmd_ty :: LHsCmdTop Name -> Int
295                -> TcM (LHsCmdTop Name, Int, TcType, TcType, TcType)
296     new_cmd_ty cmd i
297           = do  { b_ty   <- newFlexiTyVarTy arrowTyConKind
298                 ; tup_ty <- newFlexiTyVarTy liftedTypeKind
299                         -- We actually make a type variable for the tuple
300                         -- because we don't know how deeply nested it is yet    
301                 ; s_ty   <- newFlexiTyVarTy liftedTypeKind
302                 ; return (cmd, i, b_ty, tup_ty, s_ty)
303                 }
304
305     tc_cmd w_tv (cmd, i, b, tup_ty, s)
306       = do { tup_ty' <- zonkTcType tup_ty
307            ; let (corner_ty, arg_tys) = unscramble tup_ty'
308
309                 -- Check that it has the right shape:
310                 --      ((w,s1) .. sn)
311                 -- where the si do not mention w
312            ; _bogus <- unifyType corner_ty (mkTyVarTy w_tv)
313            ; checkTc (not (w_tv `elemVarSet` tyVarsOfTypes arg_tys))
314                      (badFormFun i tup_ty')
315      -- JPM: WARNING: this test is utterly bogus; see #5609
316      -- We are not using the coercion returned by the unify;
317      -- and (even more seriously) the w not in arg_tys test is totally
318      -- bogus if there are suspended equality constraints. This code
319      -- needs to be re-architected.
320
321            ; tcCmdTop (env { cmd_arr = b }) cmd arg_tys s }
322
323     unscramble :: TcType -> (TcType, [TcType])
324     -- unscramble ((w,s1) .. sn)        =  (w, [s1..sn])
325     unscramble ty = unscramble' ty []
326
327     unscramble' ty ss
328        = case tcSplitTyConApp_maybe ty of
329             Just (tc, [t,s]) | tc == pairTyCon 
330                ->  unscramble' t (s:ss)
331             _ -> (ty, ss)
332
333 -----------------------------------------------------------------
334 --              Base case for illegal commands
335 -- This is where expressions that aren't commands get rejected
336
337 tc_cmd _ cmd _
338   = failWithTc (vcat [ptext (sLit "The expression"), nest 2 (ppr cmd), 
339                       ptext (sLit "was found where an arrow command was expected")])
340 \end{code}
341
342
343 %************************************************************************
344 %*                                                                      *
345                 Stmts
346 %*                                                                      *
347 %************************************************************************
348
349 \begin{code}
350 --------------------------------
351 --      Mdo-notation
352 -- The distinctive features here are
353 --      (a) RecStmts, and
354 --      (b) no rebindable syntax
355
356 tcArrDoStmt :: CmdEnv -> TcStmtChecker
357 tcArrDoStmt env _ (LastStmt rhs _) res_ty thing_inside
358   = do  { rhs' <- tcCmd env rhs ([], res_ty)
359         ; thing <- thing_inside (panic "tcArrDoStmt")
360         ; return (LastStmt rhs' noSyntaxExpr, thing) }
361
362 tcArrDoStmt env _ (ExprStmt rhs _ _ _) res_ty thing_inside
363   = do  { (rhs', elt_ty) <- tc_arr_rhs env rhs
364         ; thing          <- thing_inside res_ty
365         ; return (ExprStmt rhs' noSyntaxExpr noSyntaxExpr elt_ty, thing) }
366
367 tcArrDoStmt env ctxt (BindStmt pat rhs _ _) res_ty thing_inside
368   = do  { (rhs', pat_ty) <- tc_arr_rhs env rhs
369         ; (pat', thing)  <- tcPat (StmtCtxt ctxt) pat pat_ty $
370                             thing_inside res_ty
371         ; return (BindStmt pat' rhs' noSyntaxExpr noSyntaxExpr, thing) }
372
373 tcArrDoStmt env ctxt (RecStmt { recS_stmts = stmts, recS_later_ids = later_names
374                             , recS_rec_ids = rec_names }) res_ty thing_inside
375   = do  { let tup_names = rec_names ++ filterOut (`elem` rec_names) later_names
376         ; tup_elt_tys <- newFlexiTyVarTys (length tup_names) liftedTypeKind
377         ; let tup_ids = zipWith mkLocalId tup_names tup_elt_tys
378         ; tcExtendIdEnv tup_ids $ do
379         { (stmts', tup_rets)
380                 <- tcStmtsAndThen ctxt (tcArrDoStmt env) stmts res_ty   $ \ _res_ty' ->
381                         -- ToDo: res_ty not really right
382                    zipWithM tcCheckId tup_names tup_elt_tys
383
384         ; thing <- thing_inside res_ty
385                 -- NB:  The rec_ids for the recursive things 
386                 --      already scope over this part. This binding may shadow
387                 --      some of them with polymorphic things with the same Name
388                 --      (see note [RecStmt] in HsExpr)
389
390         ; let rec_ids = takeList rec_names tup_ids
391         ; later_ids <- tcLookupLocalIds later_names
392
393         ; let rec_rets = takeList rec_names tup_rets
394         ; let ret_table = zip tup_ids tup_rets
395         ; let later_rets = [r | i <- later_ids, (j, r) <- ret_table, i == j]
396
397         ; return (emptyRecStmt { recS_stmts = stmts', recS_later_ids = later_ids
398                                , recS_later_rets = later_rets
399                                , recS_rec_ids = rec_ids, recS_rec_rets = rec_rets
400                                , recS_ret_ty = res_ty }, thing)
401         }}
402
403 tcArrDoStmt _ _ stmt _ _
404   = pprPanic "tcArrDoStmt: unexpected Stmt" (ppr stmt)
405
406 tc_arr_rhs :: CmdEnv -> LHsExpr Name -> TcM (LHsExpr TcId, TcType)
407 tc_arr_rhs env rhs = do { ty <- newFlexiTyVarTy liftedTypeKind
408                         ; rhs' <- tcCmd env rhs ([], ty)
409                         ; return (rhs', ty) }
410 \end{code}
411
412
413 %************************************************************************
414 %*                                                                      *
415                 Helpers
416 %*                                                                      *
417 %************************************************************************
418
419
420 \begin{code}
421 mkPairTy :: Type -> Type -> Type
422 mkPairTy t1 t2 = mkTyConApp pairTyCon [t1,t2]
423
424 arrowTyConKind :: Kind          --  *->*->*
425 arrowTyConKind = mkArrowKinds [liftedTypeKind, liftedTypeKind] liftedTypeKind
426 \end{code}
427
428
429 %************************************************************************
430 %*                                                                      *
431                 Errors
432 %*                                                                      *
433 %************************************************************************
434
435 \begin{code}
436 cmdCtxt :: HsExpr Name -> SDoc
437 cmdCtxt cmd = ptext (sLit "In the command:") <+> ppr cmd
438
439 nonEmptyCmdStkErr :: HsExpr Name -> SDoc
440 nonEmptyCmdStkErr cmd
441   = hang (ptext (sLit "Non-empty command stack at command:"))
442        2 (ppr cmd)
443
444 kappaUnderflow :: HsExpr Name -> SDoc
445 kappaUnderflow cmd
446   = hang (ptext (sLit "Command stack underflow at command:"))
447        2 (ppr cmd)
448
449 badFormFun :: Int -> TcType -> SDoc
450 badFormFun i tup_ty'
451  = hang (ptext (sLit "The type of the") <+> speakNth i <+> ptext (sLit "argument of a command form has the wrong shape"))
452       2 (ptext (sLit "Argument type:") <+> ppr tup_ty')
453 \end{code}