TcExpr.lhs 50.5 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}
8 9 10
-- The above warning supression flag is a temporary kludge.
-- While working on this module you are encouraged to remove it and fix
-- any warnings in the module. See
Ian Lynagh's avatar
Ian Lynagh committed
11
--     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings
12 13
-- for details

14
module TcExpr ( tcPolyExpr, tcPolyExprNC, tcMonoExpr, tcMonoExprNC, 
15 16
                tcInferRho, tcInferRhoNC, 
                tcSyntaxOp, tcCheckId,
17
                addExprErrCtxt ) where
18

19
#include "HsVersions.h"
20

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

26 27
import HsSyn
import TcHsSyn
28
import TcRnMonad
29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44
import TcUnify
import BasicTypes
import Inst
import TcBinds
import TcEnv
import TcArrows
import TcMatches
import TcHsType
import TcPat
import TcMType
import TcType
import Id
import DataCon
import Name
import TyCon
import Type
45
import Coercion
46 47 48
import Var
import VarSet
import TysWiredIn
49 50
import TysPrim( intPrimTy )
import PrimOp( tagToEnumKey )
51
import PrelNames
52
import DynFlags
53
import SrcLoc
54
import Util
55 56
import ListSetOps
import Maybes
57 58
import Outputable
import FastString
59
import Control.Monad
60
\end{code}
61

sof's avatar
sof committed
62 63 64 65 66 67
%************************************************************************
%*									*
\subsection{Main wrappers}
%*									*
%************************************************************************

68
\begin{code}
69
tcPolyExpr, tcPolyExprNC
70 71
	 :: LHsExpr Name	-- Expression to type check
       	 -> TcSigmaType		-- Expected type (could be a polytpye)
72 73
       	 -> TcM (LHsExpr TcId)	-- Generalised expr with expected type

74 75
-- tcPolyExpr is a convenient place (frequent but not too frequent)
-- place to add context information.
76 77 78 79
-- The NC version does not do so, usually because the caller wants
-- to do so himself.

tcPolyExpr expr res_ty 	
80
  = addExprErrCtxt expr $
81
    do { traceTc "tcPolyExpr" (ppr res_ty); tcPolyExprNC expr res_ty }
82

83 84
tcPolyExprNC expr res_ty
  = do { traceTc "tcPolyExprNC" (ppr res_ty)
85
       ; (gen_fn, expr') <- tcGen GenSigCtxt res_ty $ \ _ rho ->
86 87
			    tcMonoExprNC expr rho
       ; return (mkLHsWrap gen_fn expr') }
88 89

---------------
90
tcMonoExpr, tcMonoExprNC 
91 92 93
    :: LHsExpr Name      -- Expression to type check
    -> TcRhoType         -- Expected type (could be a type variable)
			 -- Definitely no foralls at the top
94 95 96 97 98 99 100
    -> TcM (LHsExpr TcId)

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

tcMonoExprNC (L loc expr) res_ty
101 102 103 104
  = ASSERT( not (isSigmaTy res_ty) )
    setSrcSpan loc $
    do	{ expr' <- tcExpr expr res_ty
	; return (L loc expr') }
105

106
---------------
107
tcInferRho, tcInferRhoNC :: LHsExpr Name -> TcM (LHsExpr TcId, TcRhoType)
108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128
-- 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)
sof's avatar
sof committed
129 130 131 132 133
\end{code}


%************************************************************************
%*									*
134
	tcExpr: the main expression typechecker
sof's avatar
sof committed
135 136 137 138
%*									*
%************************************************************************

\begin{code}
139
tcExpr :: HsExpr Name -> TcRhoType -> TcM (HsExpr TcId)
140 141 142
tcExpr e res_ty | debugIsOn && isSigmaTy res_ty     -- Sanity check
       	        = pprPanic "tcExpr: sigma" (ppr res_ty $$ ppr e)

143
tcExpr (HsVar name)  res_ty = tcCheckId name res_ty
144

145
tcExpr (HsApp e1 e2) res_ty = tcApp e1 [e2] res_ty
146

147 148 149 150 151 152 153 154 155
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') }
156

andy@galois.com's avatar
andy@galois.com committed
157
tcExpr (HsTickPragma info expr) res_ty 
158 159
  = do { expr' <- tcMonoExpr expr res_ty
       ; return (HsTickPragma info expr') }
160

161
tcExpr (HsCoreAnn lbl expr) res_ty
162 163 164 165
  = do	{ expr' <- tcMonoExpr expr res_ty
	; return (HsCoreAnn lbl expr') }

tcExpr (HsOverLit lit) res_ty  
166
  = do 	{ lit' <- newOverloadedLit (LiteralOrigin lit) lit res_ty
167 168 169
	; return (HsOverLit lit') }

tcExpr (NegApp expr neg_expr) res_ty
170
  = do	{ neg_expr' <- tcSyntaxOp NegateOrigin neg_expr
171 172 173
				  (mkFunTy res_ty res_ty)
	; expr' <- tcMonoExpr expr res_ty
	; return (NegApp expr' neg_expr') }
174

175
tcExpr (HsIPVar ip) res_ty
176 177
  = do	{ let origin = IPOccOrigin ip
	 	-- Implicit parameters must have a *tau-type* not a 
178 179 180
		-- type scheme.  We enforce this by creating a fresh
		-- type variable as its type.  (Because res_ty may not
		-- be a tau-type.)
181
	; ip_ty <- newFlexiTyVarTy argTypeKind	-- argTypeKind: it can't be an unboxed tuple
182 183
	; ip_var <- emitWanted origin (mkIPPred ip ip_ty)
	; tcWrapResult (HsIPVar (IPName ip_var)) ip_ty res_ty }
184

185 186
tcExpr (HsLam match) res_ty
  = do	{ (co_fn, match') <- tcMatchLambda match res_ty
187
	; return (mkHsWrap co_fn (HsLam match')) }
188

189 190 191 192 193
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') 
194
            <- tcGen ExprSigCtxt sig_tc_ty $ \ skol_tvs res_ty ->
195 196 197
      	       tcExtendTyVarEnv2 (hsExplicitTvs sig_ty `zip` mkTyVarTys skol_tvs) $
	             	       	-- See Note [More instantiated than scoped] in TcBinds
      	       tcMonoExprNC expr res_ty
198

199
      ; let inner_expr = ExprWithTySigOut (mkLHsWrap gen_fn expr') sig_ty
200

201 202
      ; (inst_wrap, rho) <- deeplyInstantiate ExprSigOrigin sig_tc_ty
      ; tcWrapResult (mkHsWrap inst_wrap inner_expr) rho res_ty }
203

204
tcExpr (HsType ty) _
205 206 207 208 209 210
  = 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*.
211 212
\end{code}

213

214 215
%************************************************************************
%*									*
216
		Infix operators and sections
217 218 219
%*									*
%************************************************************************

220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264
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 


265
\begin{code}
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
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
       ; let doc = ptext (sLit "The first argument of ($) takes")
       ; (co_arg1, [arg2_ty], op_res_ty) <- matchExpectedFunTys doc 1 arg1_ty
       	 -- arg2_ty maybe polymorphic; that's the point
       ; arg2' <- tcArg op (arg2, arg2_ty, 2)
       ; co_res <- unifyType op_res_ty res_ty
       ; op_id <- tcLookupId op_name
       ; let op' = L loc (HsWrap (mkWpTyApps [arg2_ty, op_res_ty]) (HsVar op_id))
       ; return $ mkHsWrapCoI co_res $
         OpApp (mkLHsWrapCoI co_arg1 arg1') op' fix arg2' }

  | otherwise
  = do { traceTc "Non Application rule" (ppr op)
       ; (op', op_ty) <- tcInferFun op
       ; (co_fn, arg_tys, op_res_ty) <- unifyOpFunTys op 2 op_ty
       ; co_res <- unifyType op_res_ty res_ty
       ; [arg1', arg2'] <- tcArgs op [arg1, arg2] arg_tys
       ; return $ mkHsWrapCoI co_res $
         OpApp arg1' (mkLHsWrapCoI co_fn op') fix arg2' }
299

300
-- Right sections, equivalent to \ x -> x `op` expr, or
301
--	\ x -> op x expr
302
 
303 304 305 306 307 308 309 310 311 312 313
tcExpr (SectionR op arg2) res_ty
  = do { (op', op_ty) <- tcInferFun op
       ; (co_fn, [arg1_ty, arg2_ty], op_res_ty) <- unifyOpFunTys op 2 op_ty
       ; co_res <- unifyType (mkFunTy arg1_ty op_res_ty) res_ty
       ; arg2' <- tcArg op (arg2, arg2_ty, 2)
       ; return $ mkHsWrapCoI co_res $
         SectionR (mkLHsWrapCoI co_fn op') arg2' } 

tcExpr (SectionL arg1 op) res_ty
  = do { (op', op_ty) <- tcInferFun op
       ; dflags <- getDOpts	    -- Note [Left sections]
314
       ; let n_reqd_args | xopt Opt_PostfixOperators dflags = 1
315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332
                         | otherwise                        = 2

       ; (co_fn, (arg1_ty:arg_tys), op_res_ty) <- unifyOpFunTys op n_reqd_args op_ty
       ; co_res <- unifyType (mkFunTys arg_tys op_res_ty) res_ty
       ; arg1' <- tcArg op (arg1, arg1_ty, 1)
       ; return $ mkHsWrapCoI co_res $
         SectionL arg1' (mkLHsWrapCoI co_fn op') }

tcExpr (ExplicitTuple tup_args boxity) res_ty
  | all tupArgPresent tup_args
  = do { let tup_tc = tupleTyCon boxity (length tup_args)
       ; (coi, arg_tys) <- matchExpectedTyConApp tup_tc res_ty
       ; tup_args1 <- tcTupArgs tup_args arg_tys
       ; return $ mkHsWrapCoI coi (ExplicitTuple tup_args1 boxity) }
    
  | otherwise
  = -- The tup_args are a mixture of Present and Missing (for tuple sections)
    do { let kind = case boxity of { Boxed   -> liftedTypeKind
333
                                   ; Unboxed -> argTypeKind }
334
             arity = length tup_args 
335
             tup_tc = tupleTyCon boxity arity
336 337 338

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

342 343 344 345
       ; coi <- unifyType actual_res_ty res_ty

       -- Handle tuple sections where
       ; tup_args1 <- tcTupArgs tup_args arg_tys
346
       
347 348 349 350 351 352 353 354 355 356 357 358 359 360 361
       ; return $ mkHsWrapCoI coi (ExplicitTuple tup_args1 boxity) }

tcExpr (ExplicitList _ exprs) res_ty
  = do 	{ (coi, elt_ty) <- matchExpectedListTy res_ty
	; exprs' <- mapM (tc_elt elt_ty) exprs
	; return $ mkHsWrapCoI coi (ExplicitList elt_ty exprs') }
  where
    tc_elt elt_ty expr = tcPolyExpr expr elt_ty

tcExpr (ExplicitPArr _ exprs) res_ty	-- maybe empty
  = do	{ (coi, elt_ty) <- matchExpectedPArrTy res_ty
    	; exprs' <- mapM (tc_elt elt_ty) exprs	
	; return $ mkHsWrapCoI coi (ExplicitPArr elt_ty exprs') }
  where
    tc_elt elt_ty expr = tcPolyExpr expr elt_ty
362 363
\end{code}

364 365 366 367 368 369
%************************************************************************
%*									*
		Let, case, if, do
%*									*
%************************************************************************

370
\begin{code}
371 372 373 374
tcExpr (HsLet binds expr) res_ty
  = do	{ (binds', expr') <- tcLocalBinds binds $
			     tcMonoExpr expr res_ty   
	; return (HsLet binds' expr') }
375

376 377 378 379 380 381 382 383 384 385
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
386
	  (scrut', scrut_ty) <- tcInferRho scrut
387

388
	; traceTc "HsCase" (ppr scrut_ty)
389 390
	; matches' <- tcMatchesCase match_ctxt scrut_ty matches exp_ty
	; return (HsCase scrut' matches') }
391
 where
ross's avatar
ross committed
392
    match_ctxt = MC { mc_what = CaseAlt,
393
		      mc_body = tcBody }
394

395 396 397 398 399 400
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') }

401
tcExpr (HsIf (Just fun) pred b1 b2) res_ty   -- Note [Rebindable syntax for if]
402
  = do { pred_ty <- newFlexiTyVarTy openTypeKind
403 404 405 406
       ; 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
407
       ; pred' <- tcMonoExpr pred pred_ty
408 409 410 411 412 413 414
       ; 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
415
       ; return (HsIf (Just fun') pred' b1' b2') }
416

417 418
tcExpr (HsDo do_or_lc stmts body _) res_ty
  = tcDoStmts do_or_lc stmts body res_ty
419

420
tcExpr (HsProc pat cmd) res_ty
421 422
  = do	{ (pat', cmd', coi) <- tcProc pat cmd res_ty
	; return $ mkHsWrapCoI coi (HsProc pat' cmd') }
ross's avatar
ross committed
423

424
tcExpr e@(HsArrApp _ _ _ _ _) _
Ian Lynagh's avatar
Ian Lynagh committed
425 426
  = failWithTc (vcat [ptext (sLit "The arrow command"), nest 2 (ppr e), 
                      ptext (sLit "was found where an expression was expected")])
ross's avatar
ross committed
427

428
tcExpr e@(HsArrForm _ _ _) _
Ian Lynagh's avatar
Ian Lynagh committed
429 430
  = failWithTc (vcat [ptext (sLit "The arrow command"), nest 2 (ppr e), 
                      ptext (sLit "was found where an expression was expected")])
431 432
\end{code}

433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448
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"


449 450 451 452 453 454 455
%************************************************************************
%*									*
		Record construction and update
%*									*
%************************************************************************

\begin{code}
456
tcExpr (RecordCon (L loc con_name) _ rbinds) res_ty
457
  = do	{ data_con <- tcLookupDataCon con_name
458

459
 	-- Check for missing fields
460
	; checkMissingFields data_con rbinds
461

462
	; (con_expr, con_tau) <- tcInferId con_name
463
	; let arity = dataConSourceArity data_con
464 465 466 467 468 469 470
	      (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
	; return $ mkHsWrapCoI co_res $ 
          RecordCon (L loc con_id) con_expr rbinds' } 
471
\end{code}
472

473 474 475 476
Note [Type of a record update]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The main complication with RecordUpd is that we need to explicitly
handle the *non-updated* fields.  Consider:
477

478 479 480
	data T a b c = MkT1 { fa :: a, fb :: (b,c) }
		     | MkT2 { fa :: a, fb :: (b,c), fc :: c -> c }
		     | MkT3 { fd :: a }
481
	
482
	upd :: T a b c -> (b',c) -> T a b' c
483 484
	upd t x = t { fb = x}

485 486 487 488 489
The result type should be (T a b' c)
not (T a b c),   because 'b' *is not* mentioned in a non-updated field
not (T a b' c'), becuase 'c' *is*     mentioned in a non-updated field
NB that it's not good enough to look at just one constructor; we must
look at them all; cf Trac #3219
490

491
After all, upd should be equivalent to:
492 493 494 495 496 497 498
	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).
499
We call these the "fixed" type variables, and compute them in getFixedTyVars.
500 501

Note that because MkT3 doesn't contain all the fields being updated,
502 503
its RHS is simply an error, so it doesn't impose any type constraints.
Hence the use of 'relevant_cont'.
504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526

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 }
527

528 529 530 531 532 533
The criterion we use is this:

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

534 535 536 537 538 539 540 541 542
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.)

543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574
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}
575
tcExpr (RecordUpd record_expr rbinds _ _ _) res_ty
576 577
  = ASSERT( notNull upd_fld_names )
    do	{
578
	-- STEP 0
579
	-- Check that the field names are really field names
580 581 582 583 584 585 586 587
	; 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)
588 589 590
    
	-- STEP 1
	-- Figure out the tycon and data cons from the first field name
591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608
	; 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
	      (con1_tvs, _, _, _, _, con1_arg_tys, _) = dataConFullSig con1
	      con1_flds = dataConFieldLabels con1
	      con1_res_ty = mkFamilyTyConApp tycon (mkTyVarTys con1_tvs)
   	      
simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
609
	-- Step 2
610 611
	-- Check that at least one constructor has all the named fields
	-- i.e. has an empty set of bad fields returned by badFields
612 613 614 615 616
	; 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
617
	; let flds1_w_tys = zipEqual "tcExpr:RecConUpd" con1_flds con1_arg_tys
618 619
	      upd_flds1_w_tys = filter is_updated flds1_w_tys
	      is_updated (fld,_) = fld `elem` upd_fld_names
620

621
	      bad_upd_flds = filter bad_fld upd_flds1_w_tys
622 623 624 625 626 627 628 629 630
	      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
631 632
	-- These are variables that appear in *any* arg of *any* of the
	-- relevant constructors *except* in the updated fields
633 634 635
	-- 
	; let fixed_tvs = getFixedTyVars con1_tvs relevant_cons
	      is_fixed_tv tv = tv `elemVarSet` fixed_tvs
636
	      mk_inst_ty tv result_inst_ty 
637 638
	        | is_fixed_tv tv = return result_inst_ty	    -- Same as result type
	        | otherwise      = newFlexiTyVarTy (tyVarKind tv)  -- Fresh type, of correct kind
639 640 641 642

	; (_, result_inst_tys, result_inst_env) <- tcInstTyVars con1_tvs
	; scrut_inst_tys <- zipWithM mk_inst_ty con1_tvs result_inst_tys

643
	; let rec_res_ty    = substTy result_inst_env con1_res_ty
644 645 646 647
	      con1_arg_tys' = map (substTy result_inst_env) con1_arg_tys
	      scrut_subst   = zipTopTvSubst con1_tvs scrut_inst_tys
	      scrut_ty      = substTy scrut_subst con1_res_ty

648 649
        ; co_res <- unifyType rec_res_ty res_ty

650 651 652 653 654 655 656
	-- 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)
657
	; instStupidTheta RecordUpdOrigin theta'
sof's avatar
sof committed
658

659
	-- Step 7: make a cast for the scrutinee, in the case that it's from a type family
660 661 662 663
	; let scrut_co | Just co_con <- tyConFamilyCoercion_maybe tycon 
		       = WpCast $ mkTyConApp co_con scrut_inst_tys
		       | otherwise
		       = idHsWrapper
sof's avatar
sof committed
664
	-- Phew!
665 666 667
        ; return $ mkHsWrapCoI co_res $
          RecordUpd (mkLHsWrap scrut_co record_expr') rbinds'
			           relevant_cons scrut_inst_tys result_inst_tys  }
668
  where
669 670 671
    upd_fld_names = hsRecFields rbinds

    getFixedTyVars :: [TyVar] -> [DataCon] -> TyVarSet
672
    -- These tyvars must not change across the updates
673
    getFixedTyVars tvs1 cons
674
      = mkVarSet [tv1 | con <- cons
675 676 677 678 679
    		      , let (tvs, theta, arg_tys, _) = dataConSig con
		      	    flds = dataConFieldLabels con
    			    fixed_tvs = exactTyVarsOfTypes fixed_tys
			    	    -- fixed_tys: See Note [Type of a record update]
			    	        `unionVarSet` tyVarsOfTheta theta 
680 681 682
				    -- Universally-quantified tyvars that
				    -- appear in any of the *implicit*
				    -- arguments to the constructor are fixed
683 684 685 686
			    	    -- See Note [Implict type sharing]
			    	        
		            fixed_tys = [ty | (fld,ty) <- zip flds arg_tys
                                            , not (fld `elem` upd_fld_names)]
687
                      , (tv1,tv) <- tvs1 `zip` tvs	-- Discards existentials in tvs
688
        	      , tv `elemVarSet` fixed_tvs ]
689 690 691 692 693 694 695 696 697
\end{code}

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

699
\begin{code}
700
tcExpr (ArithSeq _ seq@(From expr)) res_ty
701
  = do	{ (coi, elt_ty) <- matchExpectedListTy res_ty
702 703
	; expr' <- tcPolyExpr expr elt_ty
	; enum_from <- newMethodFromName (ArithSeqOrigin seq) 
704 705
			      enumFromName elt_ty 
	; return $ mkHsWrapCoI coi (ArithSeq enum_from (From expr')) }
706

707 708
tcExpr (ArithSeq _ seq@(FromThen expr1 expr2)) res_ty
  = do	{ (coi, elt_ty) <- matchExpectedListTy res_ty
709 710 711
	; expr1' <- tcPolyExpr expr1 elt_ty
	; expr2' <- tcPolyExpr expr2 elt_ty
	; enum_from_then <- newMethodFromName (ArithSeqOrigin seq) 
712
			      enumFromThenName elt_ty 
713
	; return $ mkHsWrapCoI coi 
714
                    (ArithSeq enum_from_then (FromThen expr1' expr2')) }
715

716 717
tcExpr (ArithSeq _ seq@(FromTo expr1 expr2)) res_ty
  = do	{ (coi, elt_ty) <- matchExpectedListTy res_ty
718 719 720
	; expr1' <- tcPolyExpr expr1 elt_ty
	; expr2' <- tcPolyExpr expr2 elt_ty
	; enum_from_to <- newMethodFromName (ArithSeqOrigin seq) 
721
		  	      enumFromToName elt_ty 
722
	; return $ mkHsWrapCoI coi 
723
                     (ArithSeq enum_from_to (FromTo expr1' expr2')) }
sof's avatar
sof committed
724

725 726
tcExpr (ArithSeq _ seq@(FromThenTo expr1 expr2 expr3)) res_ty
  = do	{ (coi, elt_ty) <- matchExpectedListTy res_ty
727 728 729 730
	; expr1' <- tcPolyExpr expr1 elt_ty
	; expr2' <- tcPolyExpr expr2 elt_ty
	; expr3' <- tcPolyExpr expr3 elt_ty
	; eft <- newMethodFromName (ArithSeqOrigin seq) 
731
		      enumFromThenToName elt_ty 
732
	; return $ mkHsWrapCoI coi 
733
                     (ArithSeq eft (FromThenTo expr1' expr2' expr3')) }
chak's avatar
chak committed
734

735 736
tcExpr (PArrSeq _ seq@(FromTo expr1 expr2)) res_ty
  = do	{ (coi, elt_ty) <- matchExpectedPArrTy res_ty
737 738 739
	; expr1' <- tcPolyExpr expr1 elt_ty
	; expr2' <- tcPolyExpr expr2 elt_ty
	; enum_from_to <- newMethodFromName (PArrSeqOrigin seq) 
740
				 enumFromToPName elt_ty 
741
	; return $ mkHsWrapCoI coi 
742
                     (PArrSeq enum_from_to (FromTo expr1' expr2')) }
chak's avatar
chak committed
743

744 745
tcExpr (PArrSeq _ seq@(FromThenTo expr1 expr2 expr3)) res_ty
  = do	{ (coi, elt_ty) <- matchExpectedPArrTy res_ty
746 747 748 749
	; expr1' <- tcPolyExpr expr1 elt_ty
	; expr2' <- tcPolyExpr expr2 elt_ty
	; expr3' <- tcPolyExpr expr3 elt_ty
	; eft <- newMethodFromName (PArrSeqOrigin seq)
750
		      enumFromThenToPName elt_ty
751
	; return $ mkHsWrapCoI coi 
752
                     (PArrSeq eft (FromThenTo expr1' expr2' expr3')) }
chak's avatar
chak committed
753

754
tcExpr (PArrSeq _ _) _ 
chak's avatar
chak committed
755 756 757
  = panic "TcExpr.tcMonoExpr: Infinite parallel array!"
    -- the parser shouldn't have generated it and the renamer shouldn't have
    -- let it through
758 759
\end{code}

760 761 762 763 764 765 766 767 768 769

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

\begin{code}
#ifdef GHCI	/* Only if bootstrapped */
	-- Rename excludes these cases otherwise
770 771
tcExpr (HsSpliceE splice) res_ty = tcSpliceExpr splice res_ty
tcExpr (HsBracket brack)  res_ty = do	{ e <- tcBracket brack res_ty
772
					; return (unLoc e) }
773
tcExpr e@(HsQuasiQuoteE _) _ =
774
    pprPanic "Should never see HsQuasiQuoteE in type checker" (ppr e)
ross's avatar
ross committed
775
#endif /* GHCI */
776 777 778 779 780 781 782 783 784 785
\end{code}


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

\begin{code}
786
tcExpr other _ = pprPanic "tcMonoExpr" (ppr other)
787 788 789
\end{code}


790 791
%************************************************************************
%*									*
792
		Applications
793 794 795
%*									*
%************************************************************************

796
\begin{code}
797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821
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

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
822 823
        ; co_res <- addErrCtxt (funResCtxt fun) $
                    unifyType actual_res_ty res_ty
824 825 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 881 882 883 884 885 886 887 888 889 890 891 892 893 894 895 896 897 898 899 900 901 902 903 904 905 906

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

        -- Assemble the result
	; let fun2 = mkLHsWrapCoI co_fun fun1
              app  = mkLHsWrapCoI co_res (foldl mkHsApp fun2 args1)

        ; 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
	; let fun2 = mkLHsWrapCoI co_fun fun1
              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
       ; fun_ty' <- zonkTcTypeCarefully fun_ty

       ; (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') }

----------------
unifyOpFunTys :: LHsExpr Name -> Arity -> TcRhoType
              -> TcM (CoercionI, [TcSigmaType], TcRhoType)	 		
-- A wrapper for matchExpectedFunTys
unifyOpFunTys op arity ty = matchExpectedFunTys herald arity ty
  where
    herald = ptext (sLit "The operator") <+> quotes (ppr op) <+> ptext (sLit "takes")

907
---------------------------
908 909 910 911 912 913 914 915 916
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 }
tcSyntaxOp _ other 	   _      = pprPanic "tcSyntaxOp" (ppr other) 
\end{code}

917

918 919 920 921 922 923 924
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.  
925

926
Here's an example where it actually makes a real difference
927

928 929
   class C t a b | t a -> b
   instance C Char a Bool
930

931 932 933 934 935 936
   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
937

938 939 940 941 942 943 944 945 946 947
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
%*									*
%************************************************************************
948 949

\begin{code}
950 951 952 953 954 955 956 957 958 959 960 961 962 963 964 965 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 995 996 997 998 999 1000 1001 1002 1003 1004
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)
1005

1006 1007 1008 1009 1010 1011 1012
  | 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'
       ; return (mkHsWrap wrap (HsVar id), substTy subst tau) }
1013
  where
1014
    (tvs, theta, tau) = tcSplitSigmaTy (idType id)
1015 1016 1017 1018 1019 1020 1021 1022 1023 1024 1025 1026 1027 1028 1029 1030 1031 1032 1033 1034 1035 1036 1037 1038 1039 1040 1041 1042 1043 1044 1045 1046 1047 1048 1049 1050 1051 1052 1053 1054 1055 1056 1057 1058 1059 1060 1061 1062 1063 1064 1065 1066
\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.

Note [No method sharing]
~~~~~~~~~~~~~~~~~~~~~~~~
The -fno-method-sharing flag controls what happens so far as the LIE
is concerned.  The default case is that for an overloaded function we 
generate a "method" Id, and add the Method Inst to the LIE.  So you get
something like
	f :: Num a => a -> a
	f = /\a (d:Num a) -> let m = (+) a d in \ (x:a) -> m x x
If you specify -fno-method-sharing, the dictionary application 
isn't shared, so we get
	f :: Num a => a -> a
	f = /\a (d:Num a) (x:a) -> (+) a d x x
This gets a bit less sharing, but
	a) it's better for RULEs involving overloaded functions
	b) perhaps fewer separated lambdas

\begin{code}
1067 1068 1069 1070 1071 1072
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)
1073

1074 1075 1076
doStupidChecks fun_id tys
  | Just con <- isDataConId_maybe fun_id   -- (a)
  = addDataConStupidTheta con tys
1077

1078 1079 1080 1081 1082
  | fun_id `hasKey` tagToEnumKey           -- (b)
  = failWithTc (ptext (sLit "tagToEnum# must appear applied to one argument"))
  
  | otherwise
  = return () -- The common case
1083 1084
\end{code}

1085 1086 1087 1088
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
1089 1090 1091 1092 1093
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.
1094 1095 1096 1097 1098 1099 1100 1101

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

1102 1103 1104 1105 1106 1107 1108
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.
1109

1110
It's all grotesquely complicated.
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
\begin{code}
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

	; return (mkHsWrapCoI coi $ HsApp fun' arg') }
1137
  where
1138 1139 1140 1141 1142 1143 1144 1145 1146 1147 1148 1149 1150 1151 1152 1153 1154 1155 1156 1157 1158 1159 1160 1161 1162 1163 1164 1165
    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]
               -> TcM (CoercionI, TyCon, [TcType])
    	-- 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) 
      = return (IdCo ty, tc, tc_args)
      | otherwise 
      = do { mb_fam <- tcLookupFamInst tc tc_args
           ; case mb_fam of 
	       Nothing -> failWithTc (tagToEnumError ty doc3)
               Just (rep_tc, rep_args) 
                   -> return ( ACo (mkSymCoercion (mkTyConApp co_tc rep_args))
                             , rep_tc, rep_args )
                 where
                   co_tc = expectJust "tcTagToEnum" $
                           tyConFamilyCoercion_maybe rep_tc }

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

1168

1169 1170
%************************************************************************
%*									*
1171
                 Template Haskell checks
1172 1173 1174
%*									*
%************************************************************************

1175
\begin{code}
1176
checkThLocalId :: Id -> ThLevel -> TcM ()
1177
#ifndef GHCI  /* GHCI and TH is off */
1178
--------------------------------------
1179
-- Check for cross-stage lifting
1180
checkThLocalId _id _bind_lvl
1181 1182 1183
  = return ()

#else	      /* GHCI and TH is on */
1184
checkThLocalId id bind_lvl 
1185
  = do	{ use_stage <- getStage	-- TH case
1186 1187
	; let use_lvl = thLevel use_stage
	; checkWellStaged (quotes (ppr id)) bind_lvl use_lvl
1188
	; traceTc "thLocalId" (ppr id <+> ppr bind_lvl <+> ppr use_stage <+> ppr use_lvl)
1189
	; when (use_lvl > bind_lvl) $
1190
          checkCrossStageLifting id bind_lvl use_stage }
1191

1192
--------------------------------------
1193
checkCrossStageLifting :: Id -> ThLevel -> ThStage -> TcM ()
1194 1195 1196 1197 1198
-- 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 |]

1199 1200
checkCrossStageLifting _ _ Comp   = return ()
checkCrossStageLifting _ _ Splice = return ()
1201

1202
checkCrossStageLifting id _ (Brack _ ps_var lie_var) 
1203
  | thTopLevelId id
1204 1205 1206 1207 1208 1209 1210 1211 1212 1213
  =	-- 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.
1214
    keepAliveTc id
1215

1216 1217
  | otherwise	-- bind_lvl = outerLevel presumably,
		-- but the Id is not bound at top level
1218 1219 1220 1221 1222 1223 1224 1225 1226
  = 	-- 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.
1227 1228
    do 	{ let id_ty = idType id
        ; checkTc (isTauTy id_ty) (polySpliceErr id)
1229 1230 1231 1232 1233
	       -- 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
1234
   
1235 1236 1237 1238
	; lift <- if isStringTy id_ty then
	       	     do { sid <- tcLookupId DsMeta.liftStringName
		     		     -- See Note [Lifting strings]
                        ; return (HsVar sid) }
1239
	          else
1240 1241 1242 1243
                     setConstraintVar lie_var	$ do  
		          -- Put the 'lift' constraint into the right LIE
                     newMethodFromName (OccurrenceOf (idName id)) 
                                       DsMeta.liftName id_ty
1244 1245
	   
		   -- Update the pending splices
1246
	; ps <- readMutVar ps_var
1247
	; writeMutVar ps_var ((idName id, nlHsApp (noLoc lift) (nlHsVar id)) : ps)
1248

1249
	; return () }
1250
#endif /* GHCI */
1251 1252
\end{code}

1253 1254 1255 1256 1257 1258 1259 1260 1261 1262 1263 1264
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 

1265 1266 1267 1268 1269 1270
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.

1271

1272 1273 1274 1275 1276 1277
%************************************************************************
%*									*
\subsection{Record bindings}
%*									*
%************************************************************************

1278 1279
Game plan for record bindings
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1280 1281 1282
1. Find the TyCon for the bindings, from the first field label.

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

1284
For each binding field = value
1285

1286 1287
3. Instantiate the field type (from the field label) using the type
   envt from step 2.
1288

1289 1290
4  Type check the value using tcArg, passing the field type as 
   the expected argument type.
1291 1292 1293 1294 1295 1296

This extends OK when the field types are universally quantified.

	
\begin{code}
tcRecordBinds
1297
	:: DataCon
1298
	-> [TcType]	-- Expected type for each field
1299 1300
	-> HsRecordBinds Name
	-> TcM (HsRecordBinds TcId)