never executed always true always false
1 {-# LANGUAGE RankNTypes #-}
2 {-# LANGUAGE TypeFamilies #-}
3
4 {-# OPTIONS_GHC -Wno-incomplete-record-updates #-}
5
6 {-
7 (c) The University of Glasgow 2006
8 (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
9
10 -}
11
12 -- | Typecheck arrow notation
13 module GHC.Tc.Gen.Arrow ( tcProc ) where
14
15 import GHC.Prelude
16
17 import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcCheckMonoExpr, tcInferRho, tcSyntaxOp
18 , tcCheckPolyExpr )
19
20 import GHC.Hs
21 import GHC.Hs.Syn.Type
22 import GHC.Tc.Errors.Types
23 import GHC.Tc.Gen.Match
24 import GHC.Tc.Gen.Head( tcCheckId )
25 import GHC.Tc.Utils.Concrete ( hasFixedRuntimeRep )
26 import GHC.Tc.Utils.TcType
27 import GHC.Tc.Utils.TcMType
28 import GHC.Tc.Gen.Bind
29 import GHC.Tc.Gen.Pat
30 import GHC.Tc.Utils.Unify
31 import GHC.Tc.Utils.Monad
32 import GHC.Tc.Utils.Env
33 import GHC.Tc.Types.Origin
34 import GHC.Tc.Types.Evidence
35 import GHC.Core.Multiplicity
36 import GHC.Types.Id( mkLocalId )
37 import GHC.Tc.Utils.Instantiate
38 import GHC.Builtin.Types
39 import GHC.Types.Var.Set
40 import GHC.Builtin.Types.Prim
41 import GHC.Types.Basic( Arity )
42 import GHC.Types.Error
43 import GHC.Types.SrcLoc
44 import GHC.Utils.Outputable
45 import GHC.Utils.Panic
46 import GHC.Utils.Misc
47
48 import Control.Monad
49
50 {-
51 Note [Arrow overview]
52 ~~~~~~~~~~~~~~~~~~~~~
53 Here's a summary of arrows and how they typecheck. First, here's
54 a cut-down syntax:
55
56 expr ::= ....
57 | proc pat cmd
58
59 cmd ::= cmd exp -- Arrow application
60 | \pat -> cmd -- Arrow abstraction
61 | (| exp cmd1 ... cmdn |) -- Arrow form, n>=0
62 | ... -- If, case in the usual way
63
64 cmd_type ::= carg_type --> type
65
66 carg_type ::= ()
67 | (type, carg_type)
68
69 Note that
70 * The 'exp' in an arrow form can mention only
71 "arrow-local" variables
72
73 * An "arrow-local" variable is bound by an enclosing
74 cmd binding form (eg arrow abstraction)
75
76 * A cmd_type is here written with a funny arrow "-->",
77 The bit on the left is a carg_type (command argument type)
78 which itself is a nested tuple, finishing with ()
79
80 * The arrow-tail operator (e1 -< e2) means
81 (| e1 <<< arr snd |) e2
82
83
84 ************************************************************************
85 * *
86 Proc
87 * *
88 ************************************************************************
89 -}
90
91 tcProc :: LPat GhcRn -> LHsCmdTop GhcRn -- proc pat -> expr
92 -> ExpRhoType -- Expected type of whole proc expression
93 -> TcM (LPat GhcTc, LHsCmdTop GhcTc, TcCoercion)
94
95 tcProc pat cmd@(L loc (HsCmdTop names _)) exp_ty
96 = do { exp_ty <- expTypeToType exp_ty -- no higher-rank stuff with arrows
97 ; (co, (exp_ty1, res_ty)) <- matchExpectedAppTy exp_ty
98 ; (co1, (arr_ty, arg_ty)) <- matchExpectedAppTy exp_ty1
99 -- start with the names as they are used to desugar the proc itself
100 -- See #17423
101 ; names' <- setSrcSpanA loc $
102 mapM (tcSyntaxName ProcOrigin arr_ty) names
103 ; let cmd_env = CmdEnv { cmd_arr = arr_ty }
104 ; (pat', cmd') <- newArrowScope
105 $ tcCheckPat (ArrowMatchCtxt ProcExpr) pat (unrestricted arg_ty)
106 $ tcCmdTop cmd_env names' cmd (unitTy, res_ty)
107 ; let res_co = mkTcTransCo co
108 (mkTcAppCo co1 (mkTcNomReflCo res_ty))
109 ; return (pat', cmd', res_co) }
110
111 {-
112 ************************************************************************
113 * *
114 Commands
115 * *
116 ************************************************************************
117 -}
118
119 -- See Note [Arrow overview]
120 type CmdType = (CmdArgType, TcTauType) -- cmd_type
121 type CmdArgType = TcTauType -- carg_type, a nested tuple
122
123 data CmdEnv
124 = CmdEnv {
125 cmd_arr :: TcType -- ^ Arrow type constructor, of kind *->*->*
126 }
127
128 mkCmdArrTy :: CmdEnv -> TcTauType -> TcTauType -> TcTauType
129 mkCmdArrTy env t1 t2 = mkAppTys (cmd_arr env) [t1, t2]
130
131 ---------------------------------------
132 tcCmdTop :: CmdEnv
133 -> CmdSyntaxTable GhcTc -- ^ Type-checked Arrow class methods (arr, (>>>), ...)
134 -> LHsCmdTop GhcRn
135 -> CmdType
136 -> TcM (LHsCmdTop GhcTc)
137
138 tcCmdTop env names (L loc (HsCmdTop _names cmd)) cmd_ty@(cmd_stk, res_ty)
139 = setSrcSpanA loc $
140 do { cmd' <- tcCmd env cmd cmd_ty
141 ; return (L loc $ HsCmdTop (CmdTopTc cmd_stk res_ty names) cmd') }
142
143 ----------------------------------------
144 tcCmd :: CmdEnv -> LHsCmd GhcRn -> CmdType -> TcM (LHsCmd GhcTc)
145 -- The main recursive function
146 tcCmd env (L loc cmd) cmd_ty@(_, res_ty)
147 = setSrcSpan (locA loc) $ do
148 { cmd' <- tc_cmd env cmd cmd_ty
149 ; _concrete_ev <- hasFixedRuntimeRep (FRRArrow $ ArrowCmdResTy cmd) res_ty
150 ; return (L loc cmd') }
151
152 tc_cmd :: CmdEnv -> HsCmd GhcRn -> CmdType -> TcM (HsCmd GhcTc)
153 tc_cmd env (HsCmdPar x lpar cmd rpar) res_ty
154 = do { cmd' <- tcCmd env cmd res_ty
155 ; return (HsCmdPar x lpar cmd' rpar) }
156
157 tc_cmd env (HsCmdLet x tkLet binds tkIn (L body_loc body)) res_ty
158 = do { (binds', body') <- tcLocalBinds binds $
159 setSrcSpan (locA body_loc) $
160 tc_cmd env body res_ty
161 ; return (HsCmdLet x tkLet binds' tkIn (L body_loc body')) }
162
163 tc_cmd env in_cmd@(HsCmdCase x scrut matches) (stk, res_ty)
164 = addErrCtxt (cmdCtxt in_cmd) $ do
165 (scrut', scrut_ty) <- tcInferRho scrut
166 matches' <- tcCmdMatches env scrut_ty matches (stk, res_ty)
167 return (HsCmdCase x scrut' matches')
168
169 tc_cmd env in_cmd@(HsCmdLamCase x matches) (stk, res_ty)
170 = addErrCtxt (cmdCtxt in_cmd) $ do
171 (co, [scrut_ty], stk') <- matchExpectedCmdArgs 1 stk
172 matches' <- tcCmdMatches env scrut_ty matches (stk', res_ty)
173 return (mkHsCmdWrap (mkWpCastN co) (HsCmdLamCase x matches'))
174
175 tc_cmd env (HsCmdIf x NoSyntaxExprRn pred b1 b2) res_ty -- Ordinary 'if'
176 = do { pred' <- tcCheckMonoExpr pred boolTy
177 ; b1' <- tcCmd env b1 res_ty
178 ; b2' <- tcCmd env b2 res_ty
179 ; return (HsCmdIf x NoSyntaxExprTc pred' b1' b2')
180 }
181
182 tc_cmd env (HsCmdIf x fun@(SyntaxExprRn {}) pred b1 b2) res_ty -- Rebindable syntax for if
183 = do { pred_ty <- newOpenFlexiTyVarTy
184 -- For arrows, need ifThenElse :: forall r. T -> r -> r -> r
185 -- because we're going to apply it to the environment, not
186 -- the return value.
187 ; (_, [r_tv]) <- tcInstSkolTyVars [alphaTyVar]
188 ; let r_ty = mkTyVarTy r_tv
189 ; checkTc (not (r_tv `elemVarSet` tyCoVarsOfType pred_ty))
190 TcRnArrowIfThenElsePredDependsOnResultTy
191 ; (pred', fun') <- tcSyntaxOp IfThenElseOrigin fun
192 (map synKnownType [pred_ty, r_ty, r_ty])
193 (mkCheckExpType r_ty) $ \ _ _ ->
194 tcCheckMonoExpr pred pred_ty
195
196 ; b1' <- tcCmd env b1 res_ty
197 ; b2' <- tcCmd env b2 res_ty
198 ; return (HsCmdIf x fun' pred' b1' b2')
199 }
200
201 -------------------------------------------
202 -- Arrow application
203 -- (f -< a) or (f -<< a)
204 --
205 -- D |- fun :: a t1 t2
206 -- D,G |- arg :: t1
207 -- ------------------------
208 -- D;G |-a fun -< arg :: stk --> t2
209 --
210 -- D,G |- fun :: a t1 t2
211 -- D,G |- arg :: t1
212 -- ------------------------
213 -- D;G |-a fun -<< arg :: stk --> t2
214 --
215 -- (plus -<< requires ArrowApply)
216
217 tc_cmd env cmd@(HsCmdArrApp _ fun arg ho_app lr) (_, res_ty)
218 = addErrCtxt (cmdCtxt cmd) $
219 do { arg_ty <- newOpenFlexiTyVarTy
220 ; let fun_ty = mkCmdArrTy env arg_ty res_ty
221 ; fun' <- select_arrow_scope (tcCheckMonoExpr fun fun_ty)
222
223 ; arg' <- tcCheckMonoExpr arg arg_ty
224
225 ; _concrete_ev <- hasFixedRuntimeRep
226 (FRRArrow $ ArrowCmdArrApp (unLoc fun) (unLoc arg) ho_app)
227 fun_ty
228
229 ; return (HsCmdArrApp fun_ty fun' arg' ho_app lr) }
230 where
231 -- Before type-checking f, use the environment of the enclosing
232 -- proc for the (-<) case.
233 -- Local bindings, inside the enclosing proc, are not in scope
234 -- inside f. In the higher-order case (-<<), they are.
235 -- See Note [Escaping the arrow scope] in GHC.Tc.Types
236 select_arrow_scope tc = case ho_app of
237 HsHigherOrderApp -> tc
238 HsFirstOrderApp -> escapeArrowScope tc
239
240 -------------------------------------------
241 -- Command application
242 --
243 -- D,G |- exp : t
244 -- D;G |-a cmd : (t,stk) --> res
245 -- -----------------------------
246 -- D;G |-a cmd exp : stk --> res
247
248 tc_cmd env cmd@(HsCmdApp x fun arg) (cmd_stk, res_ty)
249 = addErrCtxt (cmdCtxt cmd) $
250 do { arg_ty <- newOpenFlexiTyVarTy
251 ; fun' <- tcCmd env fun (mkPairTy arg_ty cmd_stk, res_ty)
252 ; arg' <- tcCheckMonoExpr arg arg_ty
253 ; _concrete_ev <- hasFixedRuntimeRep
254 (FRRArrow $ ArrowCmdApp (unLoc fun) (unLoc arg))
255 arg_ty
256 ; return (HsCmdApp x fun' arg') }
257
258 -------------------------------------------
259 -- Lambda
260 --
261 -- D;G,x:t |-a cmd : stk --> res
262 -- ------------------------------
263 -- D;G |-a (\x.cmd) : (t,stk) --> res
264
265 tc_cmd env
266 (HsCmdLam x (MG { mg_alts = L l [L mtch_loc
267 (match@(Match { m_pats = pats, m_grhss = grhss }))],
268 mg_origin = origin }))
269 (cmd_stk, res_ty)
270 = addErrCtxt (pprMatchInCtxt match) $
271 do { (co, arg_tys, cmd_stk') <- matchExpectedCmdArgs n_pats cmd_stk
272
273 -- Check the patterns, and the GRHSs inside
274 ; (pats', grhss') <- setSrcSpanA mtch_loc $
275 tcPats (ArrowMatchCtxt KappaExpr)
276 pats (map (unrestricted . mkCheckExpType) arg_tys) $
277 tc_grhss grhss cmd_stk' (mkCheckExpType res_ty)
278
279 ; let match' = L mtch_loc (Match { m_ext = noAnn
280 , m_ctxt = ArrowMatchCtxt KappaExpr
281 , m_pats = pats'
282 , m_grhss = grhss' })
283 arg_tys = map (unrestricted . hsLPatType) pats'
284
285 ; _concrete_evs <-
286 zipWithM
287 (\ (Scaled _ arg_ty) i ->
288 hasFixedRuntimeRep (FRRArrow $ ArrowCmdLam i) arg_ty)
289 arg_tys
290 [1..]
291
292 ; let
293 cmd' = HsCmdLam x (MG { mg_alts = L l [match']
294 , mg_ext = MatchGroupTc arg_tys res_ty
295 , mg_origin = origin })
296 ; return (mkHsCmdWrap (mkWpCastN co) cmd') }
297 where
298 n_pats = length pats
299 match_ctxt = ArrowMatchCtxt KappaExpr
300 pg_ctxt = PatGuard match_ctxt
301
302 tc_grhss (GRHSs x grhss binds) stk_ty res_ty
303 = do { (binds', grhss') <- tcLocalBinds binds $
304 mapM (wrapLocMA (tc_grhs stk_ty res_ty)) grhss
305 ; return (GRHSs x grhss' binds') }
306
307 tc_grhs stk_ty res_ty (GRHS x guards body)
308 = do { (guards', rhs') <- tcStmtsAndThen pg_ctxt tcGuardStmt guards res_ty $
309 \ res_ty -> tcCmd env body
310 (stk_ty, checkingExpType "tc_grhs" res_ty)
311 ; return (GRHS x guards' rhs') }
312
313 -------------------------------------------
314 -- Do notation
315
316 tc_cmd env (HsCmdDo _ (L l stmts) ) (cmd_stk, res_ty)
317 = do { co <- unifyType Nothing unitTy cmd_stk -- Expecting empty argument stack
318 ; stmts' <- tcStmts ArrowExpr (tcArrDoStmt env) stmts res_ty
319 ; return (mkHsCmdWrap (mkWpCastN co) (HsCmdDo res_ty (L l stmts') )) }
320
321
322 -----------------------------------------------------------------
323 -- Arrow ``forms'' (| e c1 .. cn |)
324 --
325 -- D; G |-a1 c1 : stk1 --> r1
326 -- ...
327 -- D; G |-an cn : stkn --> rn
328 -- D |- e :: forall e. a1 (e, stk1) t1
329 -- ...
330 -- -> an (e, stkn) tn
331 -- -> a (e, stk) t
332 -- e \not\in (stk, stk1, ..., stkm, t, t1, ..., tn)
333 -- ----------------------------------------------
334 -- D; G |-a (| e c1 ... cn |) : stk --> t
335
336 tc_cmd env cmd@(HsCmdArrForm x expr f fixity cmd_args) (cmd_stk, res_ty)
337 = addErrCtxt (cmdCtxt cmd) $
338 do { (cmd_args', cmd_tys) <- mapAndUnzipM tc_cmd_arg cmd_args
339 -- We use alphaTyVar for 'w'
340 ; let e_ty = mkInfForAllTy alphaTyVar $
341 mkVisFunTysMany cmd_tys $
342 mkCmdArrTy env (mkPairTy alphaTy cmd_stk) res_ty
343 ; expr' <- tcCheckPolyExpr expr e_ty
344 ; return (HsCmdArrForm x expr' f fixity cmd_args') }
345
346 where
347 tc_cmd_arg :: LHsCmdTop GhcRn -> TcM (LHsCmdTop GhcTc, TcType)
348 tc_cmd_arg cmd@(L loc (HsCmdTop names _))
349 = do { arr_ty <- newFlexiTyVarTy arrowTyConKind
350 ; stk_ty <- newFlexiTyVarTy liftedTypeKind
351 ; res_ty <- newFlexiTyVarTy liftedTypeKind
352 ; names' <- setSrcSpanA loc $
353 mapM (tcSyntaxName ArrowCmdOrigin arr_ty) names
354 ; let env' = env { cmd_arr = arr_ty }
355 ; cmd' <- tcCmdTop env' names' cmd (stk_ty, res_ty)
356 ; return (cmd', mkCmdArrTy env' (mkPairTy alphaTy stk_ty) res_ty) }
357
358 -----------------------------------------------------------------
359 -- Base case for illegal commands
360 -- This is where expressions that aren't commands get rejected
361
362 tc_cmd _ cmd _
363 = failWithTc (TcRnArrowCommandExpected cmd)
364
365 -- | Typechecking for case command alternatives. Used for both
366 -- 'HsCmdCase' and 'HsCmdLamCase'.
367 tcCmdMatches :: CmdEnv
368 -> TcType -- ^ type of the scrutinee
369 -> MatchGroup GhcRn (LHsCmd GhcRn) -- ^ case alternatives
370 -> CmdType
371 -> TcM (MatchGroup GhcTc (LHsCmd GhcTc))
372 tcCmdMatches env scrut_ty matches (stk, res_ty)
373 = tcMatchesCase match_ctxt (unrestricted scrut_ty) matches (mkCheckExpType res_ty)
374 where
375 match_ctxt = MC { mc_what = ArrowMatchCtxt ArrowCaseAlt,
376 mc_body = mc_body }
377 mc_body body res_ty' = do { res_ty' <- expTypeToType res_ty'
378 ; tcCmd env body (stk, res_ty') }
379
380 matchExpectedCmdArgs :: Arity -> TcType -> TcM (TcCoercionN, [TcType], TcType)
381 matchExpectedCmdArgs 0 ty
382 = return (mkTcNomReflCo ty, [], ty)
383 matchExpectedCmdArgs n ty
384 = do { (co1, [ty1, ty2]) <- matchExpectedTyConApp pairTyCon ty
385 ; (co2, tys, res_ty) <- matchExpectedCmdArgs (n-1) ty2
386 ; return (mkTcTyConAppCo Nominal pairTyCon [co1, co2], ty1:tys, res_ty) }
387
388 {-
389 ************************************************************************
390 * *
391 Stmts
392 * *
393 ************************************************************************
394 -}
395
396 --------------------------------
397 -- Mdo-notation
398 -- The distinctive features here are
399 -- (a) RecStmts, and
400 -- (b) no rebindable syntax
401
402 tcArrDoStmt :: CmdEnv -> TcCmdStmtChecker
403 tcArrDoStmt env _ (LastStmt x rhs noret _) res_ty thing_inside
404 = do { rhs' <- tcCmd env rhs (unitTy, res_ty)
405 ; thing <- thing_inside (panic "tcArrDoStmt")
406 ; return (LastStmt x rhs' noret noSyntaxExpr, thing) }
407
408 tcArrDoStmt env _ (BodyStmt _ rhs _ _) res_ty thing_inside
409 = do { (rhs', elt_ty) <- tc_arr_rhs env rhs
410 ; thing <- thing_inside res_ty
411 ; return (BodyStmt elt_ty rhs' noSyntaxExpr noSyntaxExpr, thing) }
412
413 tcArrDoStmt env ctxt (BindStmt _ pat rhs) res_ty thing_inside
414 = do { (rhs', pat_ty) <- tc_arr_rhs env rhs
415 ; (pat', thing) <- tcCheckPat (StmtCtxt ctxt) pat (unrestricted pat_ty) $
416 thing_inside res_ty
417 ; return (mkTcBindStmt pat' rhs', thing) }
418
419 tcArrDoStmt env ctxt (RecStmt { recS_stmts = L l stmts, recS_later_ids = later_names
420 , recS_rec_ids = rec_names }) res_ty thing_inside
421 = do { let tup_names = rec_names ++ filterOut (`elem` rec_names) later_names
422 ; tup_elt_tys <- newFlexiTyVarTys (length tup_names) liftedTypeKind
423 ; let tup_ids = zipWith (\n p -> mkLocalId n Many p) tup_names tup_elt_tys -- Many because it's a recursive definition
424 ; tcExtendIdEnv tup_ids $ do
425 { (stmts', tup_rets)
426 <- tcStmtsAndThen ctxt (tcArrDoStmt env) stmts res_ty $ \ _res_ty' ->
427 -- ToDo: res_ty not really right
428 zipWithM tcCheckId tup_names (map mkCheckExpType tup_elt_tys)
429
430 ; thing <- thing_inside res_ty
431 -- NB: The rec_ids for the recursive things
432 -- already scope over this part. This binding may shadow
433 -- some of them with polymorphic things with the same Name
434 -- (see note [RecStmt] in GHC.Hs.Expr)
435
436 ; let rec_ids = takeList rec_names tup_ids
437 ; later_ids <- tcLookupLocalIds later_names
438
439 ; let rec_rets = takeList rec_names tup_rets
440 ; let ret_table = zip tup_ids tup_rets
441 ; let later_rets = [r | i <- later_ids, (j, r) <- ret_table, i == j]
442
443 ; let
444 stmt :: Stmt GhcTc (LocatedA (HsCmd GhcTc))
445 stmt = emptyRecStmtId
446 { recS_stmts = L l stmts'
447 -- { recS_stmts = _ stmts'
448 , recS_later_ids = later_ids
449 , recS_rec_ids = rec_ids
450 , recS_ext = unitRecStmtTc
451 { recS_later_rets = later_rets
452 , recS_rec_rets = rec_rets
453 , recS_ret_ty = res_ty} }
454 ; return (stmt, thing)
455 }}
456
457 tcArrDoStmt _ _ stmt _ _
458 = pprPanic "tcArrDoStmt: unexpected Stmt" (ppr stmt)
459
460 tc_arr_rhs :: CmdEnv -> LHsCmd GhcRn -> TcM (LHsCmd GhcTc, TcType)
461 tc_arr_rhs env rhs = do { ty <- newFlexiTyVarTy liftedTypeKind
462 ; rhs' <- tcCmd env rhs (unitTy, ty)
463 ; return (rhs', ty) }
464
465 {-
466 ************************************************************************
467 * *
468 Helpers
469 * *
470 ************************************************************************
471 -}
472
473 mkPairTy :: Type -> Type -> Type
474 mkPairTy t1 t2 = mkTyConApp pairTyCon [t1,t2]
475
476 arrowTyConKind :: Kind -- *->*->*
477 arrowTyConKind = mkVisFunTysMany [liftedTypeKind, liftedTypeKind] liftedTypeKind
478
479 {-
480 ************************************************************************
481 * *
482 Errors
483 * *
484 ************************************************************************
485 -}
486
487 cmdCtxt :: HsCmd GhcRn -> SDoc
488 cmdCtxt cmd = text "In the command:" <+> ppr cmd