TcArrows.lhs 10.7 KB
Newer Older
1
%
Simon Marlow's avatar
Simon Marlow committed
2
% (c) The University of Glasgow 2006
3
4
% (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
%
Simon Marlow's avatar
Simon Marlow committed
5
Typecheck arrow notation
6
7
8
9

\begin{code}
module TcArrows ( tcProc ) where

10
import {-# SOURCE #-}	TcExpr( tcMonoExpr, tcInferRho, tcSyntaxOp )
11
12

import HsSyn
Simon Marlow's avatar
Simon Marlow committed
13
14
15
16
17
18
import TcMatches
import TcType
import TcMType
import TcBinds
import TcPat
import TcUnify
19
import TcRnMonad
20
import Coercion
Simon Marlow's avatar
Simon Marlow committed
21
22
23
import Inst
import Name
import TysWiredIn
24
import VarSet 
Simon Marlow's avatar
Simon Marlow committed
25
import TysPrim
26

Simon Marlow's avatar
Simon Marlow committed
27
import SrcLoc
28
import Outputable
29
import FastString
Simon Marlow's avatar
Simon Marlow committed
30
import Util
31
32

import Control.Monad
33
34
35
36
37
38
39
40
41
\end{code}

%************************************************************************
%*									*
		Proc	
%*									*
%************************************************************************

\begin{code}
42
tcProc :: InPat Name -> LHsCmdTop Name		-- proc pat -> expr
43
       -> TcRhoType				-- Expected type of whole proc expression
44
       -> TcM (OutPat TcId, LHsCmdTop TcId, CoercionI)
45
46

tcProc pat cmd exp_ty
47
  = newArrowScope $
48
49
    do	{ (coi, (exp_ty1, res_ty)) <- matchExpectedAppTy exp_ty 
	; (coi1, (arr_ty, arg_ty)) <- matchExpectedAppTy exp_ty1
ross's avatar
ross committed
50
	; let cmd_env = CmdEnv { cmd_arr = arr_ty }
51
	; (pat', cmd') <- tcPat ProcExpr pat arg_ty $
52
53
54
			  tcCmdTop cmd_env cmd [] res_ty
        ; let res_coi = mkTransCoI coi (mkAppTyCoI coi1 (IdCo res_ty))
	; return (pat', cmd', res_coi) }
55
56
57
58
59
60
61
62
63
64
65
\end{code}


%************************************************************************
%*									*
		Commands
%*									*
%************************************************************************

\begin{code}
type CmdStack = [TcTauType]
ross's avatar
ross committed
66
67
data CmdEnv
  = CmdEnv {
ross's avatar
ross committed
68
	cmd_arr		:: TcType -- arrow type constructor, of kind *->*->*
ross's avatar
ross committed
69
    }
70
71
72
73
74
75

mkCmdArrTy :: CmdEnv -> TcTauType -> TcTauType -> TcTauType
mkCmdArrTy env t1 t2 = mkAppTys (cmd_arr env) [t1, t2]

---------------------------------------
tcCmdTop :: CmdEnv 
76
         -> LHsCmdTop Name
77
         -> CmdStack
78
79
80
81
	 -> TcTauType	-- Expected result type; always a monotype
                             -- We know exactly how many cmd args are expected,
			     -- albeit perhaps not their types; so we can pass 
			     -- in a CmdStack
82
        -> TcM (LHsCmdTop TcId)
83

84
tcCmdTop env (L loc (HsCmdTop cmd _ _ names)) cmd_stk res_ty
85
  = setSrcSpan loc $
86
    do	{ cmd'   <- tcGuardedCmd env cmd cmd_stk res_ty
87
	; names' <- mapM (tcSyntaxName ProcOrigin (cmd_arr env)) names
88
	; return (L loc $ HsCmdTop cmd' cmd_stk res_ty names') }
89
90
91


----------------------------------------
92
tcGuardedCmd :: CmdEnv -> LHsExpr Name -> CmdStack
93
	     -> TcTauType -> TcM (LHsExpr TcId)
94
-- A wrapper that deals with the refinement (if any)
95
96
97
98
tcGuardedCmd env expr stk res_ty
  = do	{ body <- tcCmd env expr (stk, res_ty)
	; return body 
        }
99

100
tcCmd :: CmdEnv -> LHsExpr Name -> (CmdStack, TcTauType) -> TcM (LHsExpr TcId)
101
	-- The main recursive function
102
tcCmd env (L loc expr) res_ty
103
  = setSrcSpan loc $ do
104
105
	{ expr' <- tc_cmd env expr res_ty
	; return (L loc expr') }
106

Ian Lynagh's avatar
Ian Lynagh committed
107
tc_cmd :: CmdEnv -> HsExpr Name -> (CmdStack, TcTauType) -> TcM (HsExpr TcId)
108
tc_cmd env (HsPar cmd) res_ty
109
110
111
  = do	{ cmd' <- tcCmd env cmd res_ty
	; return (HsPar cmd') }

112
tc_cmd env (HsLet binds (L body_loc body)) res_ty
113
114
115
116
  = do	{ (binds', body') <- tcLocalBinds binds		$
			     setSrcSpan body_loc 	$
			     tc_cmd env body res_ty
	; return (HsLet binds' (L body_loc body')) }
117

118
tc_cmd env in_cmd@(HsCase scrut matches) (stk, res_ty)
119
  = addErrCtxt (cmdCtxt in_cmd) $ do
120
      (scrut', scrut_ty) <- tcInferRho scrut 
121
122
      matches' <- tcMatchesCase match_ctxt scrut_ty matches res_ty
      return (HsCase scrut' matches')
ross's avatar
ross committed
123
124
125
  where
    match_ctxt = MC { mc_what = CaseAlt,
                      mc_body = mc_body }
126
    mc_body body res_ty' = tcGuardedCmd env body stk res_ty'
ross's avatar
ross committed
127

128
129
130
131
132
133
134
135
136
137
138
tc_cmd env (HsIf mb_fun pred b1 b2) (stack_ty,res_ty)
  = do 	{ pred_ty <- newFlexiTyVarTy openTypeKind
	; b_ty <- newFlexiTyVarTy openTypeKind
        ; let if_ty = mkFunTys [pred_ty, b_ty, b_ty] res_ty
	; mb_fun' <- case mb_fun of 
              Nothing  -> return Nothing
              Just fun -> liftM Just (tcSyntaxOp IfOrigin fun if_ty)
  	; pred' <- tcMonoExpr pred pred_ty
	; b1'   <- tcCmd env b1 (stack_ty,b_ty)
	; b2'   <- tcCmd env b2 (stack_ty,b_ty)
	; return (HsIf mb_fun' pred' b1' b2')
139
140
141
142
    }

-------------------------------------------
-- 		Arrow application
ross's avatar
ross committed
143
--     	    (f -< a)   or   (f -<< a)
144

145
146
tc_cmd env cmd@(HsArrApp fun arg _ ho_app lr) (cmd_stk, res_ty)
  = addErrCtxt (cmdCtxt cmd)	$
147
    do  { arg_ty <- newFlexiTyVarTy openTypeKind
ross's avatar
ross committed
148
	; let fun_ty = mkCmdArrTy env (foldl mkPairTy arg_ty cmd_stk) res_ty
149

150
	; fun' <- select_arrow_scope (tcMonoExpr fun fun_ty)
151

152
	; arg' <- tcMonoExpr arg arg_ty
153

154
	; return (HsArrApp fun' arg' fun_ty ho_app lr) }
155
  where
ross's avatar
ross committed
156
157
	-- Before type-checking f, use the environment of the enclosing
	-- proc for the (-<) case.  
158
	-- Local bindings, inside the enclosing proc, are not in scope 
ross's avatar
ross committed
159
	-- inside f.  In the higher-order case (-<<), they are.
ross's avatar
ross committed
160
    select_arrow_scope tc = case ho_app of
161
	HsHigherOrderApp -> tc
ross's avatar
ross committed
162
	HsFirstOrderApp  -> escapeArrowScope tc
163

ross's avatar
ross committed
164
165
166
-------------------------------------------
-- 		Command application

167
tc_cmd env cmd@(HsApp fun arg) (cmd_stk, res_ty)
ross's avatar
ross committed
168
  = addErrCtxt (cmdCtxt cmd)	$
169
    do  { arg_ty <- newFlexiTyVarTy openTypeKind
ross's avatar
ross committed
170
171
172

	; fun' <- tcCmd env fun (arg_ty:cmd_stk, res_ty)

173
	; arg' <- tcMonoExpr arg arg_ty
ross's avatar
ross committed
174
175

	; return (HsApp fun' arg') }
176
177
178
179

-------------------------------------------
-- 		Lambda

Ian Lynagh's avatar
Ian Lynagh committed
180
tc_cmd env cmd@(HsLam (MatchGroup [L mtch_loc (match@(Match pats _maybe_rhs_sig grhss))] _))
181
       (cmd_stk, res_ty)
182
  = addErrCtxt (pprMatchInCtxt match_ctxt match)	$
183
184
185
186
187
188

    do	{ 	-- Check the cmd stack is big enough
	; checkTc (lengthAtLeast cmd_stk n_pats)
		  (kappaUnderflow cmd)

		-- Check the patterns, and the GRHSs inside
189
190
	; (pats', grhss') <- setSrcSpan mtch_loc		$
			     tcPats LambdaExpr pats cmd_stk	$
191
			     tc_grhss grhss res_ty
192

193
194
	; let match' = L mtch_loc (Match pats' Nothing grhss')
	; return (HsLam (MatchGroup [match'] res_ty))
195
196
197
198
199
	}

  where
    n_pats     = length pats
    stk'       = drop n_pats cmd_stk
200
    match_ctxt = (LambdaExpr :: HsMatchContext Name)	-- Maybe KappaExpr?
201
    pg_ctxt    = PatGuard match_ctxt
202

203
    tc_grhss (GRHSs grhss binds) res_ty
204
	= do { (binds', grhss') <- tcLocalBinds binds $
205
				   mapM (wrapLocM (tc_grhs res_ty)) grhss
206
	     ; return (GRHSs grhss' binds') }
207

208
    tc_grhs res_ty (GRHS guards body)
209
210
	= do { (guards', rhs') <- tcStmts pg_ctxt tcGuardStmt guards res_ty $
				  tcGuardedCmd env body stk'
211
	     ; return (GRHS guards' rhs') }
212
213
214
215

-------------------------------------------
-- 		Do notation

Ian Lynagh's avatar
Ian Lynagh committed
216
tc_cmd env cmd@(HsDo do_or_lc stmts body _ty) (cmd_stk, res_ty)
217
  = do 	{ checkTc (null cmd_stk) (nonEmptyCmdStkErr cmd)
simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
218
	; (stmts', body') <- tcStmts do_or_lc (tcMDoStmt tc_rhs) stmts res_ty $
219
			     tcGuardedCmd env body []
220
	; return (HsDo do_or_lc stmts' body' res_ty) }
221
  where
222
    tc_rhs rhs = do { ty <- newFlexiTyVarTy liftedTypeKind
223
224
		    ; rhs' <- tcCmd env rhs ([], ty)
		    ; return (rhs', ty) }
225
226
227


-----------------------------------------------------------------
ross's avatar
ross committed
228
--	Arrow ``forms''	      (| e c1 .. cn |)
229
230
231
232
233
234
--
--	G      |-b  c : [s1 .. sm] s
--	pop(G) |-   e : forall w. b ((w,s1) .. sm) s
--			        -> a ((w,t1) .. tn) t
--	e \not\in (s, s1..sm, t, t1..tn)
--	----------------------------------------------
ross's avatar
ross committed
235
--	G |-a  (| e c |)  :  [t1 .. tn] t
236

237
238
tc_cmd env cmd@(HsArrForm expr fixity cmd_args) (cmd_stk, res_ty)	
  = addErrCtxt (cmdCtxt cmd)	$
239
    do	{ cmds_w_tys <- zipWithM new_cmd_ty cmd_args [1..]
240
        ; [w_tv]     <- tcInstSkolTyVars [alphaTyVar]
241
	; let w_ty = mkTyVarTy w_tv 	-- Just a convenient starting point
242
243
244
245
246
247
248
249
250
251

		--  a ((w,t1) .. tn) t
	; let e_res_ty = mkCmdArrTy env (foldl mkPairTy w_ty cmd_stk) res_ty

	 	--   b ((w,s1) .. sm) s
		--   -> a ((w,t1) .. tn) t
	; let e_ty = mkFunTys [mkAppTys b [tup,s] | (_,_,b,tup,s) <- cmds_w_tys] 
			      e_res_ty

		-- Check expr
252
	; (inst_binds, expr') <- checkConstraints ArrowSkol [w_tv] [] $
253
                                 escapeArrowScope (tcMonoExpr expr e_ty)
254
255
256

		-- OK, now we are in a position to unscramble 
		-- the s1..sm and check each cmd
257
	; cmds' <- mapM (tc_cmd w_tv) cmds_w_tys
258

259
260
        ; let wrap = WpTyLam w_tv <.> mkWpLet inst_binds
	; return (HsArrForm (mkLHsWrap wrap expr') fixity cmds') }
261
262
263
  where
 	-- Make the types	
	--	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
268
	  = do	{ b_ty   <- newFlexiTyVarTy arrowTyConKind
		; tup_ty <- newFlexiTyVarTy liftedTypeKind
269
270
			-- We actually make a type variable for the tuple
			-- because we don't know how deeply nested it is yet    
271
		; s_ty   <- newFlexiTyVarTy liftedTypeKind
272
273
274
275
276
277
278
279
280
281
282
283
284
285
		; return (cmd, i, b_ty, tup_ty, s_ty)
		}

    tc_cmd w_tv (cmd, i, b, tup_ty, s)
      = do { tup_ty' <- zonkTcType tup_ty
	   ; let (corner_ty, arg_tys) = unscramble tup_ty'

		-- Check that it has the right shape:
		-- 	((w,s1) .. sn)
		-- where the si do not mention w
	   ; checkTc (corner_ty `tcEqType` mkTyVarTy w_tv && 
		      not (w_tv `elemVarSet` tyVarsOfTypes arg_tys))
		     (badFormFun i tup_ty')

286
	   ; tcCmdTop (env { cmd_arr = b }) cmd arg_tys s }
287
288
289

    unscramble :: TcType -> (TcType, [TcType])
    -- unscramble ((w,s1) .. sn)	=  (w, [s1..sn])
290
291
292
    unscramble ty = unscramble' ty []

    unscramble' ty ss
293
294
       = case tcSplitTyConApp_maybe ty of
	    Just (tc, [t,s]) | tc == pairTyCon 
295
296
	       ->  unscramble' t (s:ss)
	    _ -> (ty, ss)
297
298
299
300
301

-----------------------------------------------------------------
--		Base case for illegal commands
-- This is where expressions that aren't commands get rejected

Ian Lynagh's avatar
Ian Lynagh committed
302
tc_cmd _ cmd _
Ian Lynagh's avatar
Ian Lynagh committed
303
304
  = failWithTc (vcat [ptext (sLit "The expression"), nest 2 (ppr cmd), 
		      ptext (sLit "was found where an arrow command was expected")])
305
306
307
308
309
310
311
312
313
314
315
\end{code}


%************************************************************************
%*									*
		Helpers
%*									*
%************************************************************************


\begin{code}
Ian Lynagh's avatar
Ian Lynagh committed
316
mkPairTy :: Type -> Type -> Type
317
318
mkPairTy t1 t2 = mkTyConApp pairTyCon [t1,t2]

319
arrowTyConKind :: Kind		--  *->*->*
320
321
322
323
324
325
326
327
328
329
330
arrowTyConKind = mkArrowKinds [liftedTypeKind, liftedTypeKind] liftedTypeKind
\end{code}


%************************************************************************
%*									*
		Errors
%*									*
%************************************************************************

\begin{code}
Ian Lynagh's avatar
Ian Lynagh committed
331
cmdCtxt :: HsExpr Name -> SDoc
Ian Lynagh's avatar
Ian Lynagh committed
332
cmdCtxt cmd = ptext (sLit "In the command:") <+> ppr cmd
333

Ian Lynagh's avatar
Ian Lynagh committed
334
nonEmptyCmdStkErr :: HsExpr Name -> SDoc
335
nonEmptyCmdStkErr cmd
Ian Lynagh's avatar
Ian Lynagh committed
336
  = hang (ptext (sLit "Non-empty command stack at command:"))
337
       2 (ppr cmd)
338

Ian Lynagh's avatar
Ian Lynagh committed
339
kappaUnderflow :: HsExpr Name -> SDoc
340
kappaUnderflow cmd
Ian Lynagh's avatar
Ian Lynagh committed
341
  = hang (ptext (sLit "Command stack underflow at command:"))
342
       2 (ppr cmd)
343

Ian Lynagh's avatar
Ian Lynagh committed
344
badFormFun :: Int -> TcType -> SDoc
345
badFormFun i tup_ty'
Ian Lynagh's avatar
Ian Lynagh committed
346
 = hang (ptext (sLit "The type of the") <+> speakNth i <+> ptext (sLit "argument of a command form has the wrong shape"))
347
      2 (ptext (sLit "Argument type:") <+> ppr tup_ty')
348
\end{code}