TcExpr.lhs 55.7 KB
Newer Older
1
%
2
% (c) The University of Glasgow 2006
3
% (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4
%
5
\section[TcExpr]{Typecheck an expression}
6 7

\begin{code}
Ian Lynagh's avatar
Ian Lynagh committed
8 9 10 11 12 13 14
{-# OPTIONS -fno-warn-tabs #-}
-- The above warning supression flag is a temporary kludge.
-- While working on this module you are encouraged to remove it and
-- detab the module (please do the detabbing in a separate patch). See
--     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#TabsvsSpaces
-- for details

15
module TcExpr ( tcPolyExpr, tcPolyExprNC, tcMonoExpr, tcMonoExprNC, 
16 17
                tcInferRho, tcInferRhoNC, 
                tcSyntaxOp, tcCheckId,
18 19
                addExprErrCtxt) where
                
20
#include "HsVersions.h"
21

22
#ifdef GHCI 	/* Only if bootstrapped */
23
import {-# SOURCE #-}	TcSplice( tcSpliceExpr, tcBracket )
24
import qualified DsMeta
25 26
#endif

27 28
import HsSyn
import TcHsSyn
29
import TcRnMonad
30 31 32 33
import TcUnify
import BasicTypes
import Inst
import TcBinds
34
import FamInst          ( tcLookupFamInst )
35
import FamInstEnv       ( famInstAxiom, dataFamInstRepTyCon, FamInstMatch(..) )
36 37 38 39 40 41 42
import TcEnv
import TcArrows
import TcMatches
import TcHsType
import TcPat
import TcMType
import TcType
43
import DsMonad hiding (Splice)
44 45
import Id
import DataCon
46
import RdrName
47 48 49
import Name
import TyCon
import Type
50
import TcEvidence
51 52
import Var
import VarSet
53
import VarEnv
54
import TysWiredIn
55 56
import TysPrim( intPrimTy )
import PrimOp( tagToEnumKey )
57
import PrelNames
58
import DynFlags
59
import SrcLoc
60
import Util
61 62
import ListSetOps
import Maybes
63
import ErrUtils
64 65
import Outputable
import FastString
66
import Control.Monad
67
import Class(classTyCon)
68
\end{code}
69

sof's avatar
sof committed
70 71 72 73 74 75
%************************************************************************
%*									*
\subsection{Main wrappers}
%*									*
%************************************************************************

76
\begin{code}
77
tcPolyExpr, tcPolyExprNC
78 79
	 :: LHsExpr Name	-- Expression to type check
       	 -> TcSigmaType		-- Expected type (could be a polytpye)
80 81
       	 -> TcM (LHsExpr TcId)	-- Generalised expr with expected type

82 83
-- tcPolyExpr is a convenient place (frequent but not too frequent)
-- place to add context information.
84 85 86 87
-- The NC version does not do so, usually because the caller wants
-- to do so himself.

tcPolyExpr expr res_ty 	
88
  = addExprErrCtxt expr $
89
    do { traceTc "tcPolyExpr" (ppr res_ty); tcPolyExprNC expr res_ty }
90

91 92
tcPolyExprNC expr res_ty
  = do { traceTc "tcPolyExprNC" (ppr res_ty)
93
       ; (gen_fn, expr') <- tcGen GenSigCtxt res_ty $ \ _ rho ->
94 95
			    tcMonoExprNC expr rho
       ; return (mkLHsWrap gen_fn expr') }
96 97

---------------
98
tcMonoExpr, tcMonoExprNC 
99 100 101
    :: LHsExpr Name      -- Expression to type check
    -> TcRhoType         -- Expected type (could be a type variable)
			 -- Definitely no foralls at the top
102 103 104 105 106 107 108
    -> TcM (LHsExpr TcId)

tcMonoExpr expr res_ty
  = addErrCtxt (exprCtxt expr) $
    tcMonoExprNC expr res_ty

tcMonoExprNC (L loc expr) res_ty
109 110 111 112
  = ASSERT( not (isSigmaTy res_ty) )
    setSrcSpan loc $
    do	{ expr' <- tcExpr expr res_ty
	; return (L loc expr') }
113

114
---------------
115
tcInferRho, tcInferRhoNC :: LHsExpr Name -> TcM (LHsExpr TcId, TcRhoType)
116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136
-- Infer a *rho*-type.  This is, in effect, a special case
-- for ids and partial applications, so that if
--     f :: Int -> (forall a. a -> a) -> Int
-- then we can infer
--     f 3 :: (forall a. a -> a) -> Int
-- And that in turn is useful 
--  (a) for the function part of any application (see tcApp)
--  (b) for the special rule for '$'
tcInferRho expr = addErrCtxt (exprCtxt expr) (tcInferRhoNC expr)

tcInferRhoNC (L loc expr)
  = setSrcSpan loc $
    do { (expr', rho) <- tcInfExpr expr
       ; return (L loc expr', rho) }

tcInfExpr :: HsExpr Name -> TcM (HsExpr TcId, TcRhoType)
tcInfExpr (HsVar f) 	= tcInferId f
tcInfExpr (HsPar e) 	= do { (e', ty) <- tcInferRhoNC e
                             ; return (HsPar e', ty) }
tcInfExpr (HsApp e1 e2) = tcInferApp e1 [e2]                                  
tcInfExpr e             = tcInfer (tcExpr e)
137 138 139 140 141 142 143 144 145 146

tcHole :: OccName -> TcRhoType -> TcM (HsExpr TcId)
tcHole occ res_ty 
 = do { ty <- newFlexiTyVarTy liftedTypeKind
      ; name <- newSysName occ
      ; let ev = mkLocalId name ty
      ; loc <- getCtLoc HoleOrigin
      ; let can = CHoleCan { cc_ev = CtWanted ty ev, cc_loc = loc, cc_occ = occ }
      ; emitInsoluble can
      ; tcWrapResult (HsVar ev) ty res_ty }
sof's avatar
sof committed
147 148 149 150 151
\end{code}


%************************************************************************
%*									*
152
	tcExpr: the main expression typechecker
sof's avatar
sof committed
153 154 155 156
%*									*
%************************************************************************

\begin{code}
157
tcExpr :: HsExpr Name -> TcRhoType -> TcM (HsExpr TcId)
158 159 160
tcExpr e res_ty | debugIsOn && isSigmaTy res_ty     -- Sanity check
       	        = pprPanic "tcExpr: sigma" (ppr res_ty $$ ppr e)

161
tcExpr (HsVar name)  res_ty = tcCheckId name res_ty
162

163
tcExpr (HsApp e1 e2) res_ty = tcApp e1 [e2] res_ty
164

165 166 167 168 169 170 171 172 173
tcExpr (HsLit lit)   res_ty = do { let lit_ty = hsLitType lit
		     	         ; tcWrapResult (HsLit lit) lit_ty res_ty }

tcExpr (HsPar expr)  res_ty = do { expr' <- tcMonoExprNC expr res_ty
				 ; return (HsPar expr') }

tcExpr (HsSCC lbl expr) res_ty 
  = do { expr' <- tcMonoExpr expr res_ty
       ; return (HsSCC lbl expr') }
174

andy@galois.com's avatar
andy@galois.com committed
175
tcExpr (HsTickPragma info expr) res_ty 
176 177
  = do { expr' <- tcMonoExpr expr res_ty
       ; return (HsTickPragma info expr') }
178

179
tcExpr (HsCoreAnn lbl expr) res_ty
180 181 182 183
  = do	{ expr' <- tcMonoExpr expr res_ty
	; return (HsCoreAnn lbl expr') }

tcExpr (HsOverLit lit) res_ty  
184
  = do 	{ lit' <- newOverloadedLit (LiteralOrigin lit) lit res_ty
185 186 187
	; return (HsOverLit lit') }

tcExpr (NegApp expr neg_expr) res_ty
188
  = do	{ neg_expr' <- tcSyntaxOp NegateOrigin neg_expr
189 190 191
				  (mkFunTy res_ty res_ty)
	; expr' <- tcMonoExpr expr res_ty
	; return (NegApp expr' neg_expr') }
192

193 194 195 196 197 198 199 200 201 202 203 204 205 206 207
tcExpr (HsIPVar x) res_ty
  = do { let origin = IPOccOrigin x
       ; ipClass <- tcLookupClass ipClassName
           {- Implicit parameters must have a *tau-type* not a.
              type scheme.  We enforce this by creating a fresh
              type variable as its type.  (Because res_ty may not
              be a tau-type.) -}
       ; ip_ty <- newFlexiTyVarTy openTypeKind
       ; let ip_name = mkStrLitTy (hsIPNameFS x)
       ; ip_var <- emitWanted origin (mkClassPred ipClass [ip_name, ip_ty])
       ; tcWrapResult (fromDict ipClass ip_name ip_ty (HsVar ip_var)) ip_ty res_ty }
  where
  -- Coerces a dictionry for `IP "x" t` into `t`.
  fromDict ipClass x ty =
    case unwrapNewTyCon_maybe (classTyCon ipClass) of
208
      Just (_,_,ax) -> HsWrap $ WpCast $ mkTcUnbranchedAxInstCo ax [x,ty]
209
      Nothing       -> panic "The dictionary for `IP` is not a newtype?"
210

211 212
tcExpr (HsLam match) res_ty
  = do	{ (co_fn, match') <- tcMatchLambda match res_ty
213
	; return (mkHsWrap co_fn (HsLam match')) }
214

215 216 217 218 219 220 221 222
tcExpr e@(HsLamCase _ matches) res_ty
  = do	{ (co_fn, [arg_ty], body_ty) <- matchExpectedFunTys msg 1 res_ty
	; matches' <- tcMatchesCase match_ctxt arg_ty matches body_ty
	; return $ mkHsWrapCo co_fn $ HsLamCase arg_ty matches' }
  where msg = sep [ ptext (sLit "The function") <+> quotes (ppr e)
                  , ptext (sLit "requires")]
        match_ctxt = MC { mc_what = CaseAlt, mc_body = tcBody }

223 224 225 226 227
tcExpr (ExprWithTySig expr sig_ty) res_ty
 = do { sig_tc_ty <- tcHsSigType ExprSigCtxt sig_ty

      -- Remember to extend the lexical type-variable environment
      ; (gen_fn, expr') 
228
            <- tcGen ExprSigCtxt sig_tc_ty $ \ skol_tvs res_ty ->
229
      	       tcExtendTyVarEnv2 (hsExplicitTvs sig_ty `zip` skol_tvs) $
230 231
	             	       	-- See Note [More instantiated than scoped] in TcBinds
      	       tcMonoExprNC expr res_ty
232

233
      ; let inner_expr = ExprWithTySigOut (mkLHsWrap gen_fn expr') sig_ty
234

235 236
      ; (inst_wrap, rho) <- deeplyInstantiate ExprSigOrigin sig_tc_ty
      ; tcWrapResult (mkHsWrap inst_wrap inner_expr) rho res_ty }
237

238
tcExpr (HsType ty) _
239 240 241 242 243 244
  = failWithTc (text "Can't handle type argument:" <+> ppr ty)
	-- This is the syntax for type applications that I was planning
	-- but there are difficulties (e.g. what order for type args)
	-- so it's not enabled yet.
	-- Can't eliminate it altogether from the parser, because the
	-- same parser parses *patterns*.
245 246
tcExpr (HsUnboundVar v) res_ty
  = tcHole (rdrNameOcc v) res_ty
247 248
\end{code}

249

250 251
%************************************************************************
%*									*
252
		Infix operators and sections
253 254 255
%*									*
%************************************************************************

256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300
Note [Left sections]
~~~~~~~~~~~~~~~~~~~~
Left sections, like (4 *), are equivalent to
	\ x -> (*) 4 x,
or, if PostfixOperators is enabled, just
	(*) 4
With PostfixOperators we don't actually require the function to take
two arguments at all.  For example, (x `not`) means (not x); you get
postfix operators!  Not Haskell 98, but it's less work and kind of
useful.

Note [Typing rule for ($)]
~~~~~~~~~~~~~~~~~~~~~~~~~~
People write 
   runST $ blah
so much, where 
   runST :: (forall s. ST s a) -> a
that I have finally given in and written a special type-checking
rule just for saturated appliations of ($).  
  * Infer the type of the first argument
  * Decompose it; should be of form (arg2_ty -> res_ty), 
       where arg2_ty might be a polytype
  * Use arg2_ty to typecheck arg2

Note [Typing rule for seq]
~~~~~~~~~~~~~~~~~~~~~~~~~~
We want to allow
       x `seq` (# p,q #)
which suggests this type for seq:
   seq :: forall (a:*) (b:??). a -> b -> b, 
with (b:??) meaning that be can be instantiated with an unboxed tuple.
But that's ill-kinded!  Function arguments can't be unboxed tuples.
And indeed, you could not expect to do this with a partially-applied
'seq'; it's only going to work when it's fully applied.  so it turns
into 
    case x of _ -> (# p,q #)

For a while I slid by by giving 'seq' an ill-kinded type, but then
the simplifier eta-reduced an application of seq and Lint blew up 
with a kind error.  It seems more uniform to treat 'seq' as it it
was a language construct.  

See Note [seqId magic] in MkId, and 


301
\begin{code}
302 303 304 305 306 307 308 309 310 311 312 313 314 315 316
tcExpr (OpApp arg1 op fix arg2) res_ty
  | (L loc (HsVar op_name)) <- op
  , op_name `hasKey` seqIdKey		-- Note [Typing rule for seq]
  = do { arg1_ty <- newFlexiTyVarTy liftedTypeKind
       ; let arg2_ty = res_ty
       ; arg1' <- tcArg op (arg1, arg1_ty, 1)
       ; arg2' <- tcArg op (arg2, arg2_ty, 2)
       ; op_id <- tcLookupId op_name
       ; let op' = L loc (HsWrap (mkWpTyApps [arg1_ty, arg2_ty]) (HsVar op_id))
       ; return $ OpApp arg1' op' fix arg2' }

  | (L loc (HsVar op_name)) <- op
  , op_name `hasKey` dollarIdKey	-- Note [Typing rule for ($)]
  = do { traceTc "Application rule" (ppr op)
       ; (arg1', arg1_ty) <- tcInferRho arg1
317

318 319
       ; let doc = ptext (sLit "The first argument of ($) takes")
       ; (co_arg1, [arg2_ty], op_res_ty) <- matchExpectedFunTys doc 1 arg1_ty
320 321
         -- arg1_ty = arg2_ty -> op_res_ty
       	 -- And arg2_ty maybe polymorphic; that's the point
322 323 324

       -- Make sure that the argument and result types have kind '*'
       -- Eg we do not want to allow  (D#  $  4.0#)   Trac #5570
325 326 327
       --    (which gives a seg fault)
       -- We do this by unifying with a MetaTv; but of course
       -- it must allow foralls in the type it unifies with (hence PolyTv)!
328

329 330 331
       -- ($) :: forall ab. (a->b) -> a -> b
       ; a_ty <- newPolyFlexiTyVarTy
       ; b_ty <- newPolyFlexiTyVarTy
332
       ; arg2' <- tcArg op (arg2, arg2_ty, 2)
333

334 335 336 337 338 339 340 341 342 343 344
       ; co_res <- unifyType b_ty res_ty        -- b ~ res
       ; co_a   <- unifyType arg2_ty   a_ty     -- arg2 ~ a
       ; co_b   <- unifyType op_res_ty b_ty     -- op_res ~ b
       ; op_id  <- tcLookupId op_name

       ; let op' = L loc (HsWrap (mkWpTyApps [a_ty, b_ty]) (HsVar op_id))
       ; return $ mkHsWrapCo (co_res) $
         OpApp (mkLHsWrapCo (mkTcFunCo co_a co_b) $
                mkLHsWrapCo co_arg1 arg1') 
               op' fix 
               (mkLHsWrapCo co_a arg2') }
345 346 347 348

  | otherwise
  = do { traceTc "Non Application rule" (ppr op)
       ; (op', op_ty) <- tcInferFun op
batterseapower's avatar
batterseapower committed
349
       ; (co_fn, arg_tys, op_res_ty) <- unifyOpFunTysWrap op 2 op_ty
350 351
       ; co_res <- unifyType op_res_ty res_ty
       ; [arg1', arg2'] <- tcArgs op [arg1, arg2] arg_tys
352 353
       ; return $ mkHsWrapCo co_res $
         OpApp arg1' (mkLHsWrapCo co_fn op') fix arg2' }
354

355
-- Right sections, equivalent to \ x -> x `op` expr, or
356
--	\ x -> op x expr
357
 
358 359
tcExpr (SectionR op arg2) res_ty
  = do { (op', op_ty) <- tcInferFun op
batterseapower's avatar
batterseapower committed
360
       ; (co_fn, [arg1_ty, arg2_ty], op_res_ty) <- unifyOpFunTysWrap op 2 op_ty
361 362
       ; co_res <- unifyType (mkFunTy arg1_ty op_res_ty) res_ty
       ; arg2' <- tcArg op (arg2, arg2_ty, 2)
363 364
       ; return $ mkHsWrapCo co_res $
         SectionR (mkLHsWrapCo co_fn op') arg2' } 
365 366 367

tcExpr (SectionL arg1 op) res_ty
  = do { (op', op_ty) <- tcInferFun op
368
       ; dflags <- getDynFlags	    -- Note [Left sections]
369
       ; let n_reqd_args | xopt Opt_PostfixOperators dflags = 1
370 371
                         | otherwise                        = 2

batterseapower's avatar
batterseapower committed
372
       ; (co_fn, (arg1_ty:arg_tys), op_res_ty) <- unifyOpFunTysWrap op n_reqd_args op_ty
373 374
       ; co_res <- unifyType (mkFunTys arg_tys op_res_ty) res_ty
       ; arg1' <- tcArg op (arg1, arg1_ty, 1)
375 376
       ; return $ mkHsWrapCo co_res $
         SectionL arg1' (mkLHsWrapCo co_fn op') }
377 378 379

tcExpr (ExplicitTuple tup_args boxity) res_ty
  | all tupArgPresent tup_args
batterseapower's avatar
batterseapower committed
380
  = do { let tup_tc = tupleTyCon (boxityNormalTupleSort boxity) (length tup_args)
381 382
       ; (coi, arg_tys) <- matchExpectedTyConApp tup_tc res_ty
       ; tup_args1 <- tcTupArgs tup_args arg_tys
383
       ; return $ mkHsWrapCo coi (ExplicitTuple tup_args1 boxity) }
384 385 386 387
    
  | otherwise
  = -- The tup_args are a mixture of Present and Missing (for tuple sections)
    do { let kind = case boxity of { Boxed   -> liftedTypeKind
388
                                   ; Unboxed -> openTypeKind }
389
             arity = length tup_args 
batterseapower's avatar
batterseapower committed
390
             tup_tc = tupleTyCon (boxityNormalTupleSort boxity) arity
391 392 393

       ; arg_tys <- newFlexiTyVarTys (tyConArity tup_tc) kind
       ; let actual_res_ty
394 395 396
                 = mkFunTys [ty | (ty, Missing _) <- arg_tys `zip` tup_args]
                            (mkTyConApp tup_tc arg_tys)

397 398 399 400
       ; coi <- unifyType actual_res_ty res_ty

       -- Handle tuple sections where
       ; tup_args1 <- tcTupArgs tup_args arg_tys
401
       
402
       ; return $ mkHsWrapCo coi (ExplicitTuple tup_args1 boxity) }
403

404 405 406 407 408 409 410 411 412 413 414 415
tcExpr (ExplicitList _ witness exprs) res_ty   
  = case witness of
      Nothing   -> do  { (coi, elt_ty) <- matchExpectedListTy res_ty
                       ; exprs' <- mapM (tc_elt elt_ty) exprs                       
                       ; return $ mkHsWrapCo coi (ExplicitList elt_ty Nothing exprs') }

      Just fln -> do  { list_ty <- newFlexiTyVarTy liftedTypeKind
                     ; fln' <- tcSyntaxOp ListOrigin fln (mkFunTys [intTy, list_ty] res_ty)
                     ; (coi, elt_ty) <- matchExpectedListTy list_ty
                     ; exprs' <- mapM (tc_elt elt_ty) exprs
                     ; return $ mkHsWrapCo coi (ExplicitList elt_ty (Just fln') exprs') }
     where tc_elt elt_ty expr = tcPolyExpr expr elt_ty          
416 417 418 419

tcExpr (ExplicitPArr _ exprs) res_ty	-- maybe empty
  = do	{ (coi, elt_ty) <- matchExpectedPArrTy res_ty
    	; exprs' <- mapM (tc_elt elt_ty) exprs	
420
	; return $ mkHsWrapCo coi (ExplicitPArr elt_ty exprs') }
421 422
  where
    tc_elt elt_ty expr = tcPolyExpr expr elt_ty
423 424
\end{code}

425 426 427 428 429 430
%************************************************************************
%*									*
		Let, case, if, do
%*									*
%************************************************************************

431
\begin{code}
432 433 434 435
tcExpr (HsLet binds expr) res_ty
  = do	{ (binds', expr') <- tcLocalBinds binds $
			     tcMonoExpr expr res_ty   
	; return (HsLet binds' expr') }
436

437 438 439 440 441 442 443 444 445 446
tcExpr (HsCase scrut matches) exp_ty
  = do	{  -- We used to typecheck the case alternatives first.
	   -- The case patterns tend to give good type info to use
	   -- when typechecking the scrutinee.  For example
	   --	case (map f) of
	   --	  (x:xs) -> ...
	   -- will report that map is applied to too few arguments
	   --
	   -- But now, in the GADT world, we need to typecheck the scrutinee
	   -- first, to get type info that may be refined in the case alternatives
447
	  (scrut', scrut_ty) <- tcInferRho scrut
448

449
	; traceTc "HsCase" (ppr scrut_ty)
450 451
	; matches' <- tcMatchesCase match_ctxt scrut_ty matches exp_ty
	; return (HsCase scrut' matches') }
452
 where
453
    match_ctxt = MC { mc_what = CaseAlt,
454
		      mc_body = tcBody }
455

456 457 458 459 460 461
tcExpr (HsIf Nothing pred b1 b2) res_ty	   -- Ordinary 'if'
  = do { pred' <- tcMonoExpr pred boolTy
       ; b1' <- tcMonoExpr b1 res_ty
       ; b2' <- tcMonoExpr b2 res_ty
       ; return (HsIf Nothing pred' b1' b2') }

462
tcExpr (HsIf (Just fun) pred b1 b2) res_ty   -- Note [Rebindable syntax for if]
463
  = do { pred_ty <- newFlexiTyVarTy openTypeKind
464 465 466 467
       ; b1_ty   <- newFlexiTyVarTy openTypeKind
       ; b2_ty   <- newFlexiTyVarTy openTypeKind
       ; let if_ty = mkFunTys [pred_ty, b1_ty, b2_ty] res_ty
       ; fun'  <- tcSyntaxOp IfOrigin fun if_ty
468
       ; pred' <- tcMonoExpr pred pred_ty
469 470 471 472 473 474 475
       ; b1'   <- tcMonoExpr b1 b1_ty
       ; b2'   <- tcMonoExpr b2 b2_ty
       -- Fundamentally we are just typing (ifThenElse e1 e2 e3)
       -- so maybe we should use the code for function applications
       -- (which would allow ifThenElse to be higher rank).
       -- But it's a little awkward, so I'm leaving it alone for now
       -- and it maintains uniformity with other rebindable syntax
476
       ; return (HsIf (Just fun') pred' b1' b2') }
477

478 479 480 481 482
tcExpr (HsMultiIf _ alts) res_ty
  = do { alts' <- mapM (wrapLocM $ tcGRHS match_ctxt res_ty) alts
       ; return $ HsMultiIf res_ty alts' }
  where match_ctxt = MC { mc_what = IfAlt, mc_body = tcBody }

483 484
tcExpr (HsDo do_or_lc stmts _) res_ty
  = tcDoStmts do_or_lc stmts res_ty
485

486
tcExpr (HsProc pat cmd) res_ty
487
  = do	{ (pat', cmd', coi) <- tcProc pat cmd res_ty
488
	; return $ mkHsWrapCo coi (HsProc pat' cmd') }
489 490
\end{code}

491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506
Note [Rebindable syntax for if]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The rebindable syntax for 'if' uses the most flexible possible type
for conditionals:
  ifThenElse :: p -> b1 -> b2 -> res
to support expressions like this:

 ifThenElse :: Maybe a -> (a -> b) -> b -> b
 ifThenElse (Just a) f _ = f a  ifThenElse Nothing  _ e = e

 example :: String
 example = if Just 2
              then \v -> show v
              else "No value"


507 508 509 510 511 512 513
%************************************************************************
%*									*
		Record construction and update
%*									*
%************************************************************************

\begin{code}
514
tcExpr (RecordCon (L loc con_name) _ rbinds) res_ty
515
  = do	{ data_con <- tcLookupDataCon con_name
516

517
 	-- Check for missing fields
518
	; checkMissingFields data_con rbinds
519

520
	; (con_expr, con_tau) <- tcInferId con_name
521
	; let arity = dataConSourceArity data_con
522 523 524 525 526
	      (arg_tys, actual_res_ty) = tcSplitFunTysN con_tau arity
	      con_id = dataConWrapId data_con

        ; co_res <- unifyType actual_res_ty res_ty
        ; rbinds' <- tcRecordBinds data_con arg_tys rbinds
527
	; return $ mkHsWrapCo co_res $ 
528
          RecordCon (L loc con_id) con_expr rbinds' } 
529
\end{code}
530

531 532 533 534
Note [Type of a record update]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The main complication with RecordUpd is that we need to explicitly
handle the *non-updated* fields.  Consider:
535

536 537 538
	data T a b c = MkT1 { fa :: a, fb :: (b,c) }
		     | MkT2 { fa :: a, fb :: (b,c), fc :: c -> c }
		     | MkT3 { fd :: a }
539
	
540
	upd :: T a b c -> (b',c) -> T a b' c
541 542
	upd t x = t { fb = x}

543 544
The result type should be (T a b' c)
not (T a b c),   because 'b' *is not* mentioned in a non-updated field
Gabor Greif's avatar
typos  
Gabor Greif committed
545
not (T a b' c'), because 'c' *is*     mentioned in a non-updated field
546 547
NB that it's not good enough to look at just one constructor; we must
look at them all; cf Trac #3219
548

549
After all, upd should be equivalent to:
550 551 552 553 554 555 556
	upd t x = case t of 
			MkT1 p q -> MkT1 p x
			MkT2 a b -> MkT2 p b
			MkT3 d   -> error ...

So we need to give a completely fresh type to the result record,
and then constrain it by the fields that are *not* updated ("p" above).
557
We call these the "fixed" type variables, and compute them in getFixedTyVars.
558 559

Note that because MkT3 doesn't contain all the fields being updated,
560 561
its RHS is simply an error, so it doesn't impose any type constraints.
Hence the use of 'relevant_cont'.
562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584

Note [Implict type sharing]
~~~~~~~~~~~~~~~~~~~~~~~~~~~
We also take into account any "implicit" non-update fields.  For example
	data T a b where { MkT { f::a } :: T a a; ... }
So the "real" type of MkT is: forall ab. (a~b) => a -> T a b

Then consider
	upd t x = t { f=x }
We infer the type
	upd :: T a b -> a -> T a b
	upd (t::T a b) (x::a)
	   = case t of { MkT (co:a~b) (_:a) -> MkT co x }
We can't give it the more general type
	upd :: T a b -> c -> T c b

Note [Criteria for update]
~~~~~~~~~~~~~~~~~~~~~~~~~~
We want to allow update for existentials etc, provided the updated
field isn't part of the existential. For example, this should be ok.
  data T a where { MkT { f1::a, f2::b->b } :: T a }
  f :: T a -> b -> T b
  f t b = t { f1=b }
585

586 587 588 589 590 591
The criterion we use is this:

  The types of the updated fields
  mention only the universally-quantified type variables
  of the data constructor

592 593 594 595 596 597 598 599 600
NB: this is not (quite) the same as being a "naughty" record selector
(See Note [Naughty record selectors]) in TcTyClsDecls), at least 
in the case of GADTs. Consider
   data T a where { MkT :: { f :: a } :: T [a] }
Then f is not "naughty" because it has a well-typed record selector.
But we don't allow updates for 'f'.  (One could consider trying to
allow this, but it makes my head hurt.  Badly.  And no one has asked
for it.)

601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632
In principle one could go further, and allow
  g :: T a -> T a
  g t = t { f2 = \x -> x }
because the expression is polymorphic...but that seems a bridge too far.

Note [Data family example]
~~~~~~~~~~~~~~~~~~~~~~~~~~
    data instance T (a,b) = MkT { x::a, y::b }
  --->
    data :TP a b = MkT { a::a, y::b }
    coTP a b :: T (a,b) ~ :TP a b

Suppose r :: T (t1,t2), e :: t3
Then  r { x=e } :: T (t3,t1)
  --->
      case r |> co1 of
	MkT x y -> MkT e y |> co2
      where co1 :: T (t1,t2) ~ :TP t1 t2
	    co2 :: :TP t3 t2 ~ T (t3,t2)
The wrapping with co2 is done by the constructor wrapper for MkT

Outgoing invariants
~~~~~~~~~~~~~~~~~~~
In the outgoing (HsRecordUpd scrut binds cons in_inst_tys out_inst_tys):

  * cons are the data constructors to be updated

  * in_inst_tys, out_inst_tys have same length, and instantiate the
	*representation* tycon of the data cons.  In Note [Data 
	family example], in_inst_tys = [t1,t2], out_inst_tys = [t3,t2]
	
\begin{code}
633
tcExpr (RecordUpd record_expr rbinds _ _ _) res_ty
634 635
  = ASSERT( notNull upd_fld_names )
    do	{
636
	-- STEP 0
637
	-- Check that the field names are really field names
638 639 640 641 642 643 644 645
	; sel_ids <- mapM tcLookupField upd_fld_names
			-- The renamer has already checked that
			-- selectors are all in scope
	; let bad_guys = [ setSrcSpan loc $ addErrTc (notSelector fld_name) 
		       	 | (fld, sel_id) <- rec_flds rbinds `zip` sel_ids,
		       	   not (isRecordSelector sel_id), 	-- Excludes class ops
		       	   let L loc fld_name = hsRecFieldId fld ]
	; unless (null bad_guys) (sequence bad_guys >> failM)
646 647 648
    
	-- STEP 1
	-- Figure out the tycon and data cons from the first field name
649 650 651 652 653 654 655 656 657 658 659 660 661 662
	; let	-- It's OK to use the non-tc splitters here (for a selector)
	      sel_id : _  = sel_ids
	      (tycon, _)  = recordSelectorFieldLabel sel_id	-- We've failed already if
	      data_cons   = tyConDataCons tycon			-- it's not a field label
	      	-- NB: for a data type family, the tycon is the instance tycon

	      relevant_cons   = filter is_relevant data_cons
	      is_relevant con = all (`elem` dataConFieldLabels con) upd_fld_names
		-- A constructor is only relevant to this process if
		-- it contains *all* the fields that are being updated
		-- Other ones will cause a runtime error if they occur

		-- Take apart a representative constructor
	      con1 = ASSERT( not (null relevant_cons) ) head relevant_cons
663
	      (con1_tvs, _, _, _, con1_arg_tys, _) = dataConFullSig con1
664 665 666
	      con1_flds = dataConFieldLabels con1
	      con1_res_ty = mkFamilyTyConApp tycon (mkTyVarTys con1_tvs)
   	      
simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
667
	-- Step 2
668 669
	-- Check that at least one constructor has all the named fields
	-- i.e. has an empty set of bad fields returned by badFields
670 671 672 673 674
	; checkTc (not (null relevant_cons)) (badFieldsUpd rbinds)

	-- STEP 3    Note [Criteria for update]
	-- Check that each updated field is polymorphic; that is, its type
	-- mentions only the universally-quantified variables of the data con
675
	; let flds1_w_tys = zipEqual "tcExpr:RecConUpd" con1_flds con1_arg_tys
676 677
	      upd_flds1_w_tys = filter is_updated flds1_w_tys
	      is_updated (fld,_) = fld `elem` upd_fld_names
678

679
	      bad_upd_flds = filter bad_fld upd_flds1_w_tys
680 681 682 683 684 685 686 687 688
	      con1_tv_set = mkVarSet con1_tvs
	      bad_fld (fld, ty) = fld `elem` upd_fld_names &&
				      not (tyVarsOfType ty `subVarSet` con1_tv_set)
	; checkTc (null bad_upd_flds) (badFieldTypes bad_upd_flds)

	-- STEP 4  Note [Type of a record update]
	-- Figure out types for the scrutinee and result
	-- Both are of form (T a b c), with fresh type variables, but with
	-- common variables where the scrutinee and result must have the same type
689 690
	-- These are variables that appear in *any* arg of *any* of the
	-- relevant constructors *except* in the updated fields
691 692 693
	-- 
	; let fixed_tvs = getFixedTyVars con1_tvs relevant_cons
	      is_fixed_tv tv = tv `elemVarSet` fixed_tvs
694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712

              mk_inst_ty :: TvSubst -> (TKVar, TcType) -> TcM (TvSubst, TcType)
              -- Deals with instantiation of kind variables
              --   c.f. TcMType.tcInstTyVarsX
	      mk_inst_ty subst (tv, result_inst_ty)
	        | is_fixed_tv tv   -- Same as result type
                = return (extendTvSubst subst tv result_inst_ty, result_inst_ty)
	        | otherwise        -- Fresh type, of correct kind
                = do { new_ty <- newFlexiTyVarTy (TcType.substTy subst (tyVarKind tv))
                     ; return (extendTvSubst subst tv new_ty, new_ty) }

	; (_, result_inst_tys, result_subst) <- tcInstTyVars con1_tvs

        ; (scrut_subst, scrut_inst_tys) <- mapAccumLM mk_inst_ty emptyTvSubst 
                                                      (con1_tvs `zip` result_inst_tys) 

	; let rec_res_ty    = TcType.substTy result_subst con1_res_ty
	      scrut_ty      = TcType.substTy scrut_subst  con1_res_ty
	      con1_arg_tys' = map (TcType.substTy result_subst) con1_arg_tys
713

714 715
        ; co_res <- unifyType rec_res_ty res_ty

716 717 718 719 720 721 722
	-- STEP 5
	-- Typecheck the thing to be updated, and the bindings
	; record_expr' <- tcMonoExpr record_expr scrut_ty
	; rbinds'      <- tcRecordBinds con1 con1_arg_tys' rbinds
	
	-- STEP 6: Deal with the stupid theta
	; let theta' = substTheta scrut_subst (dataConStupidTheta con1)
723
	; instStupidTheta RecordUpdOrigin theta'
sof's avatar
sof committed
724

725
	-- Step 7: make a cast for the scrutinee, in the case that it's from a type family
726
	; let scrut_co | Just co_con <- tyConFamilyCoercion_maybe tycon 
727
		       = WpCast (mkTcUnbranchedAxInstCo co_con scrut_inst_tys)
728 729
		       | otherwise
		       = idHsWrapper
sof's avatar
sof committed
730
	-- Phew!
731
        ; return $ mkHsWrapCo co_res $
732 733
          RecordUpd (mkLHsWrap scrut_co record_expr') rbinds'
			           relevant_cons scrut_inst_tys result_inst_tys  }
734
  where
735 736 737
    upd_fld_names = hsRecFields rbinds

    getFixedTyVars :: [TyVar] -> [DataCon] -> TyVarSet
738
    -- These tyvars must not change across the updates
739
    getFixedTyVars tvs1 cons
740
      = mkVarSet [tv1 | con <- cons
741 742 743 744
    		      , let (tvs, theta, arg_tys, _) = dataConSig con
		      	    flds = dataConFieldLabels con
    			    fixed_tvs = exactTyVarsOfTypes fixed_tys
			    	    -- fixed_tys: See Note [Type of a record update]
batterseapower's avatar
batterseapower committed
745
			    	        `unionVarSet` tyVarsOfTypes theta 
746 747 748
				    -- Universally-quantified tyvars that
				    -- appear in any of the *implicit*
				    -- arguments to the constructor are fixed
749 750 751 752
			    	    -- See Note [Implict type sharing]
			    	        
		            fixed_tys = [ty | (fld,ty) <- zip flds arg_tys
                                            , not (fld `elem` upd_fld_names)]
753
                      , (tv1,tv) <- tvs1 `zip` tvs	-- Discards existentials in tvs
754
        	      , tv `elemVarSet` fixed_tvs ]
755 756 757 758 759 760 761 762 763
\end{code}

%************************************************************************
%*									*
	Arithmetic sequences			e.g. [a,b..]
	and their parallel-array counterparts	e.g. [: a,b.. :]
		
%*									*
%************************************************************************
sof's avatar
sof committed
764

765
\begin{code}
766 767
tcExpr (ArithSeq _ witness seq) res_ty
  = tcArithSeq witness seq res_ty
768

769 770
tcExpr (PArrSeq _ seq@(FromTo expr1 expr2)) res_ty
  = do	{ (coi, elt_ty) <- matchExpectedPArrTy res_ty
771 772
	; expr1' <- tcPolyExpr expr1 elt_ty
	; expr2' <- tcPolyExpr expr2 elt_ty
773
	; enumFromToP <- initDsTc $ dsDPHBuiltin enumFromToPVar
774
	; enum_from_to <- newMethodFromName (PArrSeqOrigin seq) 
775
				 (idName enumFromToP) elt_ty
776
	; return $ mkHsWrapCo coi 
777
                     (PArrSeq enum_from_to (FromTo expr1' expr2')) }
778

779 780
tcExpr (PArrSeq _ seq@(FromThenTo expr1 expr2 expr3)) res_ty
  = do	{ (coi, elt_ty) <- matchExpectedPArrTy res_ty
781 782 783
	; expr1' <- tcPolyExpr expr1 elt_ty
	; expr2' <- tcPolyExpr expr2 elt_ty
	; expr3' <- tcPolyExpr expr3 elt_ty
784
	; enumFromThenToP <- initDsTc $ dsDPHBuiltin enumFromThenToPVar
785
	; eft <- newMethodFromName (PArrSeqOrigin seq)
786
		      (idName enumFromThenToP) elt_ty        -- !!!FIXME: chak
787
	; return $ mkHsWrapCo coi 
788
                     (PArrSeq eft (FromThenTo expr1' expr2' expr3')) }
789

790
tcExpr (PArrSeq _ _) _ 
791
  = panic "TcExpr.tcExpr: Infinite parallel array!"
792 793
    -- the parser shouldn't have generated it and the renamer shouldn't have
    -- let it through
794 795
\end{code}

796 797 798 799 800 801 802 803 804 805

%************************************************************************
%*									*
		Template Haskell
%*									*
%************************************************************************

\begin{code}
#ifdef GHCI	/* Only if bootstrapped */
	-- Rename excludes these cases otherwise
806
tcExpr (HsSpliceE splice) res_ty = tcSpliceExpr splice res_ty
807
tcExpr (HsBracket brack)  res_ty = tcBracket brack res_ty
808
tcExpr e@(HsQuasiQuoteE _) _ =
809
    pprPanic "Should never see HsQuasiQuoteE in type checker" (ppr e)
810
#endif /* GHCI */
811 812 813 814 815 816 817 818 819 820
\end{code}


%************************************************************************
%*									*
		Catch-all
%*									*
%************************************************************************

\begin{code}
821
tcExpr other _ = pprPanic "tcMonoExpr" (ppr other)
822
  -- Include ArrForm, ArrApp, which shouldn't appear at all
823 824 825
\end{code}


826 827 828 829 830 831 832 833 834 835 836 837 838 839 840 841 842 843 844 845 846 847 848 849 850 851 852 853 854 855 856 857 858 859 860 861 862 863 864 865 866 867 868 869 870 871 872 873 874 875 876 877 878 879 880
%************************************************************************
%*									*
		Arithmetic sequences [a..b] etc
%*									*
%************************************************************************

\begin{code}
tcArithSeq :: Maybe (SyntaxExpr Name) -> ArithSeqInfo Name -> TcRhoType
           -> TcM (HsExpr TcId)

tcArithSeq witness seq@(From expr) res_ty
  = do { (coi, elt_ty, wit') <- arithSeqEltType witness res_ty
       ; expr' <- tcPolyExpr expr elt_ty
       ; enum_from <- newMethodFromName (ArithSeqOrigin seq) 
			      enumFromName elt_ty 
       ; return $ mkHsWrapCo coi (ArithSeq enum_from wit' (From expr')) }
     
tcArithSeq witness seq@(FromThen expr1 expr2) res_ty
  = do { (coi, elt_ty, wit') <- arithSeqEltType witness res_ty
       ; expr1' <- tcPolyExpr expr1 elt_ty
       ; expr2' <- tcPolyExpr expr2 elt_ty
       ; enum_from_then <- newMethodFromName (ArithSeqOrigin seq) 
			      enumFromThenName elt_ty 
       ; return $ mkHsWrapCo coi (ArithSeq enum_from_then wit' (FromThen expr1' expr2')) }
     
tcArithSeq witness seq@(FromTo expr1 expr2) res_ty
  = do { (coi, elt_ty, wit') <- arithSeqEltType witness res_ty
       ; expr1' <- tcPolyExpr expr1 elt_ty
       ; expr2' <- tcPolyExpr expr2 elt_ty
       ; enum_from_to <- newMethodFromName (ArithSeqOrigin seq) 
			      enumFromToName elt_ty 
       ; return $ mkHsWrapCo coi (ArithSeq enum_from_to wit' (FromTo expr1' expr2')) }

tcArithSeq witness seq@(FromThenTo expr1 expr2 expr3) res_ty
  = do { (coi, elt_ty, wit') <- arithSeqEltType witness res_ty
        ; expr1' <- tcPolyExpr expr1 elt_ty
        ; expr2' <- tcPolyExpr expr2 elt_ty
        ; expr3' <- tcPolyExpr expr3 elt_ty
        ; eft <- newMethodFromName (ArithSeqOrigin seq) 
			      enumFromThenToName elt_ty
        ; return $ mkHsWrapCo coi (ArithSeq eft wit' (FromThenTo expr1' expr2' expr3')) }

-----------------
arithSeqEltType :: Maybe (SyntaxExpr Name) -> TcRhoType 
              -> TcM (TcCoercion, TcType, Maybe (SyntaxExpr Id))
arithSeqEltType Nothing res_ty
  = do { (coi, elt_ty) <- matchExpectedListTy res_ty
       ; return (coi, elt_ty, Nothing) }
arithSeqEltType (Just fl) res_ty
  = do { list_ty <- newFlexiTyVarTy liftedTypeKind
       ; fl' <- tcSyntaxOp ListOrigin fl (mkFunTy list_ty res_ty)
       ; (coi, elt_ty) <- matchExpectedListTy list_ty
       ; return (coi, elt_ty, Just fl') }
\end{code}

881 882
%************************************************************************
%*									*
883
		Applications
884 885 886
%*									*
%************************************************************************

887
\begin{code}
888 889 890 891 892 893 894 895 896 897 898 899 900 901
tcApp :: LHsExpr Name -> [LHsExpr Name] -- Function and args
      -> TcRhoType -> TcM (HsExpr TcId) -- Translated fun and args

tcApp (L _ (HsPar e)) args res_ty
  = tcApp e args res_ty

tcApp (L _ (HsApp e1 e2)) args res_ty
  = tcApp e1 (e2:args) res_ty	-- Accumulate the arguments

tcApp (L loc (HsVar fun)) args res_ty
  | fun `hasKey` tagToEnumKey
  , [arg] <- args
  = tcTagToEnum loc fun arg res_ty

902 903 904 905
  | fun `hasKey` seqIdKey
  , [arg1,arg2] <- args
  = tcSeq loc fun arg1 arg2 res_ty

906 907 908 909 910 911 912 913 914 915 916
tcApp fun args res_ty
  = do	{   -- Type-check the function
	; (fun1, fun_tau) <- tcInferFun fun

	    -- Extract its argument types
	; (co_fun, expected_arg_tys, actual_res_ty)
	      <- matchExpectedFunTys (mk_app_msg fun) (length args) fun_tau

	-- Typecheck the result, thereby propagating 
        -- info (if any) from result into the argument types
        -- Both actual_res_ty and res_ty are deeply skolemised
917
        ; co_res <- addErrCtxtM (funResCtxt fun actual_res_ty res_ty) $
918
                    unifyType actual_res_ty res_ty
919 920 921 922 923

	-- Typecheck the arguments
	; args1 <- tcArgs fun args expected_arg_tys

        -- Assemble the result
924 925
	; let fun2 = mkLHsWrapCo co_fun fun1
              app  = mkLHsWrapCo co_res (foldl mkHsApp fun2 args1)
926 927 928 929 930 931 932 933 934 935 936 937 938 939 940 941 942 943 944 945 946

        ; return (unLoc app) }


mk_app_msg :: LHsExpr Name -> SDoc
mk_app_msg fun = sep [ ptext (sLit "The function") <+> quotes (ppr fun)
                     , ptext (sLit "is applied to")]

----------------
tcInferApp :: LHsExpr Name -> [LHsExpr Name] -- Function and args
           -> TcM (HsExpr TcId, TcRhoType) -- Translated fun and args

tcInferApp (L _ (HsPar e))     args = tcInferApp e args
tcInferApp (L _ (HsApp e1 e2)) args = tcInferApp e1 (e2:args)
tcInferApp fun args
  = -- Very like the tcApp version, except that there is
    -- no expected result type passed in
    do	{ (fun1, fun_tau) <- tcInferFun fun
	; (co_fun, expected_arg_tys, actual_res_ty)
	      <- matchExpectedFunTys (mk_app_msg fun) (length args) fun_tau
	; args1 <- tcArgs fun args expected_arg_tys
947
	; let fun2 = mkLHsWrapCo co_fun fun1
948 949 950 951 952 953 954 955 956 957 958 959 960 961 962 963 964
              app  = foldl mkHsApp fun2 args1
        ; return (unLoc app, actual_res_ty) }

----------------
tcInferFun :: LHsExpr Name -> TcM (LHsExpr TcId, TcRhoType)
-- Infer and instantiate the type of a function
tcInferFun (L loc (HsVar name)) 
  = do { (fun, ty) <- setSrcSpan loc (tcInferId name)
       	       -- Don't wrap a context around a plain Id
       ; return (L loc fun, ty) }

tcInferFun fun
  = do { (fun, fun_ty) <- tcInfer (tcMonoExpr fun)

         -- Zonk the function type carefully, to expose any polymorphism
	 -- E.g. (( \(x::forall a. a->a). blah ) e)
	 -- We can see the rank-2 type of the lambda in time to genrealise e
965
       ; fun_ty' <- zonkTcType fun_ty
966 967 968 969 970 971 972 973 974 975 976 977 978 979 980 981 982 983 984 985 986 987 988 989 990 991 992 993 994

       ; (wrap, rho) <- deeplyInstantiate AppOrigin fun_ty'
       ; return (mkLHsWrap wrap fun, rho) }

----------------
tcArgs :: LHsExpr Name				-- The function (for error messages)
       -> [LHsExpr Name] -> [TcSigmaType]	-- Actual arguments and expected arg types
       -> TcM [LHsExpr TcId]			-- Resulting args

tcArgs fun args expected_arg_tys
  = mapM (tcArg fun) (zip3 args expected_arg_tys [1..])

----------------
tcArg :: LHsExpr Name				-- The function (for error messages)
       -> (LHsExpr Name, TcSigmaType, Int)	-- Actual argument and expected arg type
       -> TcM (LHsExpr TcId)			-- Resulting argument
tcArg fun (arg, ty, arg_no) = addErrCtxt (funAppCtxt fun arg arg_no)
				 	 (tcPolyExprNC arg ty)

----------------
tcTupArgs :: [HsTupArg Name] -> [TcSigmaType] -> TcM [HsTupArg TcId]
tcTupArgs args tys 
  = ASSERT( equalLength args tys ) mapM go (args `zip` tys)
  where
    go (Missing {},   arg_ty) = return (Missing arg_ty)
    go (Present expr, arg_ty) = do { expr' <- tcPolyExpr expr arg_ty
			           ; return (Present expr') }

----------------
batterseapower's avatar
batterseapower committed
995
unifyOpFunTysWrap :: LHsExpr Name -> Arity -> TcRhoType
996
                  -> TcM (TcCoercion, [TcSigmaType], TcRhoType)	 		
997
-- A wrapper for matchExpectedFunTys
batterseapower's avatar
batterseapower committed
998
unifyOpFunTysWrap op arity ty = matchExpectedFunTys herald arity ty
999 1000 1001
  where
    herald = ptext (sLit "The operator") <+> quotes (ppr op) <+> ptext (sLit "takes")

1002
---------------------------
1003 1004 1005 1006 1007 1008
tcSyntaxOp :: CtOrigin -> HsExpr Name -> TcType -> TcM (HsExpr TcId)
-- Typecheck a syntax operator, checking that it has the specified type
-- The operator is always a variable at this stage (i.e. renamer output)
-- This version assumes res_ty is a monotype
tcSyntaxOp orig (HsVar op) res_ty = do { (expr, rho) <- tcInferIdWithOrig orig op
                                       ; tcWrapResult expr rho res_ty }
1009
tcSyntaxOp _ other 	   _      = pprPanic "tcSyntaxOp" (ppr other) 
1010 1011
\end{code}

1012

1013 1014 1015 1016 1017 1018 1019
Note [Push result type in]
~~~~~~~~~~~~~~~~~~~~~~~~~~
Unify with expected result before type-checking the args so that the
info from res_ty percolates to args.  This is when we might detect a
too-few args situation.  (One can think of cases when the opposite
order would give a better error message.) 
experimenting with putting this first.  
1020

1021
Here's an example where it actually makes a real difference
1022

1023 1024
   class C t a b | t a -> b
   instance C Char a Bool
1025

1026 1027 1028 1029 1030 1031
   data P t a = forall b. (C t a b) => MkP b
   data Q t   = MkQ (forall a. P t a)

   f1, f2 :: Q Char;
   f1 = MkQ (MkP True)
   f2 = MkQ (MkP True :: forall a. P Char a)
sof's avatar
sof committed
1032

1033 1034 1035 1036 1037 1038 1039 1040 1041 1042
With the change, f1 will type-check, because the 'Char' info from
the signature is propagated into MkQ's argument. With the check
in the other order, the extra signature in f2 is reqd.


%************************************************************************
%*									*
                 tcInferId
%*									*
%************************************************************************
1043 1044

\begin{code}
1045 1046 1047 1048 1049 1050 1051 1052 1053 1054 1055 1056 1057 1058 1059 1060 1061 1062 1063 1064 1065 1066 1067 1068 1069 1070 1071 1072 1073 1074 1075 1076 1077 1078 1079 1080 1081 1082 1083 1084 1085 1086 1087 1088 1089 1090 1091 1092 1093 1094 1095 1096 1097 1098 1099
tcCheckId :: Name -> TcRhoType -> TcM (HsExpr TcId)
tcCheckId name res_ty = do { (expr, rho) <- tcInferId name
                           ; tcWrapResult expr rho res_ty }

------------------------
tcInferId :: Name -> TcM (HsExpr TcId, TcRhoType)
-- Infer type, and deeply instantiate
tcInferId n = tcInferIdWithOrig (OccurrenceOf n) n

------------------------
tcInferIdWithOrig :: CtOrigin -> Name -> TcM (HsExpr TcId, TcRhoType)
-- Look up an occurrence of an Id, and instantiate it (deeply)

tcInferIdWithOrig orig id_name
  = do { id <- lookup_id
       ; (id_expr, id_rho) <- instantiateOuter orig id
       ; (wrap, rho) <- deeplyInstantiate orig id_rho
       ; return (mkHsWrap wrap id_expr, rho) }
  where
    lookup_id :: TcM TcId
    lookup_id 
       = do { thing <- tcLookup id_name
	    ; case thing of
    	    	 ATcId { tct_id = id, tct_level = lvl }
	           -> do { check_naughty id        -- Note [Local record selectors]
                         ; checkThLocalId id lvl
                         ; return id }

    	    	 AGlobal (AnId id) 
                   -> do { check_naughty id; return id }
	    	 	-- A global cannot possibly be ill-staged
	    	 	-- nor does it need the 'lifting' treatment
                        -- hence no checkTh stuff here

    	    	 AGlobal (ADataCon con) -> return (dataConWrapId con)

    	    	 other -> failWithTc (bad_lookup other) }

    bad_lookup thing = ppr thing <+> ptext (sLit "used where a value identifer was expected")

    check_naughty id 
      | isNaughtyRecordSelector id = failWithTc (naughtyRecordSel id)
      | otherwise		   = return ()

------------------------
instantiateOuter :: CtOrigin -> TcId -> TcM (HsExpr TcId, TcSigmaType)
-- Do just the first level of instantiation of an Id
--   a) Deal with method sharing
--   b) Deal with stupid checks
-- Only look at the *outer level* of quantification
-- See Note [Multiple instantiation]

instantiateOuter orig id
  | null tvs && null theta
  = return (HsVar id, tau)
1100

1101 1102 1103 1104 1105 1106
  | otherwise
  = do { (_, tys, subst) <- tcInstTyVars tvs
       ; doStupidChecks id tys
       ; let theta' = substTheta subst theta
       ; traceTc "Instantiating" (ppr id <+> text "with" <+> (ppr tys $$ ppr theta'))
       ; wrap <- instCall orig tys theta'
1107
       ; return (mkHsWrap wrap (HsVar id), TcType.substTy subst tau) }
1108
  where
1109
    (tvs, theta, tau) = tcSplitSigmaTy (idType id)
1110 1111 1112 1113 1114 1115 1116 1117 1118 1119 1120 1121 1122 1123 1124 1125 1126 1127 1128 1129 1130 1131 1132 1133 1134 1135 1136 1137 1138 1139 1140 1141 1142 1143 1144 1145
\end{code}

Note [Multiple instantiation]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We are careful never to make a MethodInst that has, as its meth_id, another MethodInst.
For example, consider
	f :: forall a. Eq a => forall b. Ord b => a -> b
At a call to f, at say [Int, Bool], it's tempting to translate the call to 

	f_m1
  where
	f_m1 :: forall b. Ord b => Int -> b
	f_m1 = f Int dEqInt

	f_m2 :: Int -> Bool
	f_m2 = f_m1 Bool dOrdBool

But notice that f_m2 has f_m1 as its meth_id.  Now the danger is that if we do
a tcSimplCheck with a Given f_mx :: f Int dEqInt, we may make a binding
	f_m1 = f_mx
But it's entirely possible that f_m2 will continue to float out, because it
mentions no type variables.  Result, f_m1 isn't in scope.

Here's a concrete example that does this (test tc200):

    class C a where
      f :: Eq b => b -> a -> Int
      baz :: Eq a => Int -> a -> Int

    instance C Int where
      baz = f

Current solution: only do the "method sharing" thing for the first type/dict
application, not for the iterated ones.  A horribly subtle point.

\begin{code}
1146 1147 1148 1149 1150 1151
doStupidChecks :: TcId
	       -> [TcType]
	       -> TcM ()
-- Check two tiresome and ad-hoc cases
-- (a) the "stupid theta" for a data con; add the constraints
--     from the "stupid theta" of a data constructor (sigh)
1152

1153 1154 1155
doStupidChecks fun_id tys
  | Just con <- isDataConId_maybe fun_id   -- (a)
  = addDataConStupidTheta con tys
1156

1157 1158 1159 1160 1161
  | fun_id `hasKey` tagToEnumKey           -- (b)
  = failWithTc (ptext (sLit "tagToEnum# must appear applied to one argument"))
  
  | otherwise
  = return () -- The common case
1162 1163
\end{code}

1164 1165 1166 1167
Note [tagToEnum#]
~~~~~~~~~~~~~~~~~
Nasty check to ensure that tagToEnum# is applied to a type that is an
enumeration TyCon.  Unification may refine the type later, but this
1168 1169 1170 1171 1172
check won't see that, alas.  It's crude, because it relies on our
knowing *now* that the type is ok, which in turn relies on the
eager-unification part of the type checker pushing enough information
here.  In theory the Right Thing to do is to have a new form of 
constraint but I definitely cannot face that!  And it works ok as-is.
1173 1174 1175 1176 1177 1178 1179 1180

Here's are two cases that should fail
 	f :: forall a. a
	f = tagToEnum# 0	-- Can't do tagToEnum# at a type variable

	g :: Int
	g = tagToEnum# 0	-- Int is not an enumeration

1181 1182 1183 1184 1185 1186 1187
When data type families are involved it's a bit more complicated.
     data family F a
     data instance F [Int] = A | B | C
Then we want to generate something like
     tagToEnum# R:FListInt 3# |> co :: R:FListInt ~ F [Int]
Usually that coercion is hidden inside the wrappers for 
constructors of F [Int] but here we have to do it explicitly.
1188

1189
It's all grotesquely complicated.
1190

1191
\begin{code}
1192 1193 1194 1195 1196 1197 1198 1199 1200 1201 1202 1203
tcSeq :: SrcSpan -> Name -> LHsExpr Name -> LHsExpr Name 
      -> TcRhoType -> TcM (HsExpr TcId)
-- (seq e1 e2) :: res_ty
-- We need a special typing rule because res_ty can be unboxed
tcSeq loc fun_name arg1 arg2 res_ty
  = do	{ fun <- tcLookupId fun_name
        ; (arg1', arg1_ty) <- tcInfer (tcMonoExpr arg1)
        ; arg2' <- tcMonoExpr arg2 res_ty
        ; let fun'    = L loc (HsWrap ty_args (HsVar fun))
              ty_args = WpTyApp res_ty <.> WpTyApp arg1_ty
        ; return (HsApp (L loc (HsApp fun' arg1')) arg2') }

1204 1205 1206 1207 1208 1209 1210 1211 1212 1213 1214 1215 1216 1217 1218 1219 1220 1221 1222 1223 1224 1225 1226
tcTagToEnum :: SrcSpan -> Name -> LHsExpr Name -> TcRhoType -> TcM (HsExpr TcId)
-- tagToEnum# :: forall a. Int# -> a
-- See Note [tagToEnum#]   Urgh!
tcTagToEnum loc fun_name arg res_ty
  = do	{ fun <- tcLookupId fun_name
        ; ty' <- zonkTcType res_ty

	-- Check that the type is algebraic
        ; let mb_tc_app = tcSplitTyConApp_maybe ty'
              Just (tc, tc_args) = mb_tc_app
	; checkTc (isJust mb_tc_app)
                  (tagToEnumError ty' doc1)

	-- Look through any type family
        ; (coi, rep_tc, rep_args) <- get_rep_ty ty' tc tc_args

	; checkTc (isEnumerationTyCon rep_tc) 
                  (tagToEnumError ty' doc2)

        ; arg' <- tcMonoExpr arg intPrimTy
        ; let fun' = L loc (HsWrap (WpTyApp rep_ty) (HsVar fun))
              rep_ty = mkTyConApp rep_tc rep_args

1227
	; return (mkHsWrapCo coi $ HsApp fun' arg') }
1228
  where
1229 1230 1231 1232 1233 1234
    doc1 = vcat [ ptext (sLit "Specify the type by giving a type signature")
		, ptext (sLit "e.g. (tagToEnum# x) :: Bool") ]
    doc2 = ptext (sLit "Result type must be an enumeration type")
    doc3 = ptext (sLit "No family instance for this type")

    get_rep_ty :: TcType -> TyCon -> [TcType]
1235
               -> TcM (TcCoercion, TyCon, [TcType])
1236 1237 1238 1239
    	-- Converts a family type (eg F [a]) to its rep type (eg FList a)
	-- and returns a coercion between the two
    get_rep_ty ty tc tc_args
      | not (isFamilyTyCon tc) 
1240
      = return (mkTcReflCo ty, tc, tc_args)
1241 1242 1243 1244
      | otherwise 
      = do { mb_fam <- tcLookupFamInst tc tc_args
           ; case mb_fam of 
	       Nothing -> failWithTc (tagToEnumError ty doc3)
1245 1246 1247 1248
               Just (FamInstMatch { fim_instance = rep_fam
                                  , fim_index    = index
                                  , fim_tys      = rep_args })
                   -> return ( mkTcSymCo (mkTcAxInstCo co_tc index rep_args)
1249 1250
                             , rep_tc, rep_args )
                 where
1251 1252
                   co_tc  = famInstAxiom rep_fam
                   rep_tc = dataFamInstRepTyCon rep_fam }
1253 1254 1255 1256 1257 1258

tagToEnumError :: TcType -> SDoc -> SDoc
tagToEnumError ty what
  = hang (ptext (sLit "Bad call to tagToEnum#") 
           <+> ptext (sLit "at type") <+> ppr ty) 
	 2 what
1259 1260
\end{code}

1261

1262 1263
%************************************************************************
%*									*
1264
                 Template Haskell checks
1265 1266 1267
%*									*
%************************************************************************

1268
\begin{code}
1269
checkThLocalId :: Id -> ThLevel -> TcM ()
1270
#ifndef GHCI  /* GHCI and TH is off */
1271
--------------------------------------
1272
-- Check for cross-stage lifting
1273
checkThLocalId _id _bind_lvl
1274 1275 1276
  = return ()

#else	      /* GHCI and TH is on */
1277
checkThLocalId id bind_lvl 
1278
  = do	{ use_stage <- getStage	-- TH case
1279 1280
	; let use_lvl = thLevel use_stage
	; checkWellStaged (quotes (ppr id)) bind_lvl use_lvl
1281
	; traceTc "thLocalId" (ppr id <+> ppr bind_lvl <+> ppr use_stage <+> ppr use_lvl)
1282
	; when (use_lvl > bind_lvl) $
1283
          checkCrossStageLifting id bind_lvl use_stage }
1284

1285
--------------------------------------
1286
checkCrossStageLifting :: Id -> ThLevel -> ThStage -> TcM ()
1287 1288 1289 1290 1291
-- We are inside brackets, and (use_lvl > bind_lvl)
-- Now we must check whether there's a cross-stage lift to do
-- Examples   \x -> [| x |]  
--            [| map |]

1292 1293
checkCrossStageLifting _ _ Comp   = return ()
checkCrossStageLifting _ _ Splice = return ()
1294

1295
checkCrossStageLifting id _ (Brack _ ps_var lie_var) 
1296
  | thTopLevelId id
1297 1298 1299 1300 1301 1302 1303 1304 1305 1306
  =	-- Top-level identifiers in this module,
	-- (which have External Names)
	-- are just like the imported case:
	-- no need for the 'lifting' treatment
	-- E.g.  this is fine:
	--   f x = x
	--   g y = [| f 3 |]
	-- But we do need to put f into the keep-alive
	-- set, because after desugaring the code will
	-- only mention f's *name*, not f itself.
1307
    keepAliveTc id
1308

1309 1310
  | otherwise	-- bind_lvl = outerLevel presumably,
		-- but the Id is not bound at top level
1311 1312 1313 1314 1315 1316 1317 1318 1319
  = 	-- Nested identifiers, such as 'x' in
	-- E.g. \x -> [| h x |]
	-- We must behave as if the reference to x was
	--	h $(lift x)	
	-- We use 'x' itself as the splice proxy, used by 
	-- the desugarer to stitch it all back together.
	-- If 'x' occurs many times we may get many identical
	-- bindings of the same splice proxy, but that doesn't
	-- matter, although it's a mite untidy.
1320 1321
    do 	{ let id_ty = idType id
        ; checkTc (isTauTy id_ty) (polySpliceErr id)
1322 1323 1324 1325 1326
	       -- If x is polymorphic, its occurrence sites might
	       -- have different instantiations, so we can't use plain
	       -- 'x' as the splice proxy name.  I don't know how to 
	       -- solve this, and it's probably unimportant, so I'm
	       -- just going to flag an error for now
1327
   
1328 1329 1330 1331
	; lift <- if isStringTy id_ty then
	       	     do { sid <- tcLookupId DsMeta.liftStringName
		     		     -- See Note [Lifting strings]
                        ; return (HsVar sid) }
1332
	          else
1333 1334 1335 1336
                     setConstraintVar lie_var	$ do  
		          -- Put the 'lift' constraint into the right LIE
                     newMethodFromName (OccurrenceOf (idName id)) 
                                       DsMeta.liftName id_ty
1337 1338
	   
		   -- Update the pending splices
1339
	; ps <- readMutVar ps_var
1340
	; writeMutVar ps_var ((idName id, nlHsApp (noLoc lift) (nlHsVar id)) : ps)
1341

1342
	; return () }
1343
#endif /* GHCI */
1344 1345
\end{code}

1346 1347 1348 1349 1350 1351 1352 1353 1354 1355 1356 1357
Note [Lifting strings]
~~~~~~~~~~~~~~~~~~~~~~
If we see $(... [| s |] ...) where s::String, we don't want to
generate a mass of Cons (CharL 'x') (Cons (CharL 'y') ...)) etc.
So this conditional short-circuits the lifting mechanism to generate
(liftString "xy") in that case.  I didn't want to use overlapping instances
for the Lift class in TH.Syntax, because that can lead to overlapping-instance
errors in a polymorphic situation.  

If this check fails (which isn't impossible) we get another chance; see
Note [Converting strings] in Convert.lhs 

1358 1359 1360 1361 1362 1363
Local record selectors
~~~~~~~~~~~~~~~~~~~~~~
Record selectors for TyCons in this module are ordinary local bindings,
which show up as ATcIds rather than AGlobals.  So we need to check for
naughtiness in both branches.  c.f. TcTyClsBindings.mkAuxBinds.

1364

1365 1366 1367 1368 1369 1370
%************************************************************************
%*									*
\subsection{Record bindings}
%*									*
%************************************************************************

1371 1372
Game plan for record bindings
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1373 1374 1375
1. Find the TyCon for the bindings, from the first field label.

2. Instantiate its tyvars and unify (T a1 .. an) with expected_ty.
1376

1377
For each binding field = value
1378

1379 1380
3. Instantiate the field type (from the field label) using the type
   envt from step 2.
1381

1382 1383
4  Type check the value using tcArg, passing the field type as 
   the expected argument type.
1384 1385 1386 1387 1388 1389

This extends OK when the field types are universally quantified.

	
\begin{code}
tcRecordBinds
1390
	:: DataCon
1391
	-> [TcType]	-- Expected type for each field
1392 1393
	-> HsRecordBinds Name
	-> TcM (HsRecordBinds TcId)
1394

1395
tcRecordBinds data_con arg_tys (HsRecFields rbinds dd)
1396
  = do	{ mb_binds <- mapM do_bind rbinds
1397
	; return (HsRecFields (catMaybes mb_binds) dd) }
1398
  where
1399
    flds_w_tys = zipEqual "tcRecordBinds" (dataConFieldLabels data_con) arg_tys
1400
    do_bind fld@(HsRecField { hsRecFieldId = L loc field_lbl, hsRecFieldArg = rhs })
1401
      | Just field_ty <- assocMaybe flds_w_tys field_lbl
1402
      = addErrCtxt (fieldCtxt field_lbl)	$
1403 1404 1405
	do { rhs' <- tcPolyExprNC rhs field_ty
	   ; let field_id = mkUserLocal (nameOccName field_lbl)
				        (nameUnique field_lbl)
1406 1407 1408 1409 1410
					field_ty loc 
		-- Yuk: the field_id has the *unique* of the selector Id
		-- 	    (so we can find it easily)
		--      but is a LocalId with the appropriate type of the RHS
		--	    (so the desugarer knows the type of local binder to make)
1411
	   ; return (Just (fld { hsRecFieldId = L loc field_id, hsRecFieldArg = rhs' })) }
1412 1413 1414
      | otherwise
      = do { addErrTc (badFieldCon data_con field_lbl)
	   ; return Nothing }
1415

1416
checkMissingFields :: DataCon -> HsRecordBinds Name -> TcM ()
1417 1418 1419
checkMissingFields data_con rbinds
  | null field_labels 	-- Not declared as a record;
			-- But C{} is still valid if no strict fields
1420
  = if any isBanged field_strs then
1421 1422 1423
	-- Illegal if any arg is strict
	addErrTc (missingStrictFields data_con [])
    else
1424
	return ()
1425
			
1426 1427 1428
  | otherwise = do		-- A record
    unless (null missing_s_fields)
	   (addErrTc (missingStrictFields data_con missing_s_fields))
1429