[project @ 2001-12-28 17:25:31 by simonpj]
[ghc-hetmet.git] / ghc / compiler / typecheck / TcMType.lhs
1 %
2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
3 %
4 \section{Monadic type operations}
5
6 This module contains monadic operations over types that contain mutable type variables
7
8 \begin{code}
9 module TcMType (
10   TcTyVar, TcKind, TcType, TcTauType, TcThetaType, TcTyVarSet,
11
12   --------------------------------
13   -- Creating new mutable type variables
14   newTyVar, newHoleTyVarTy,
15   newTyVarTy,           -- Kind -> NF_TcM TcType
16   newTyVarTys,          -- Int -> Kind -> NF_TcM [TcType]
17   newKindVar, newKindVars, newBoxityVar,
18   putTcTyVar, getTcTyVar,
19
20   --------------------------------
21   -- Instantiation
22   tcInstTyVar, tcInstTyVars,
23   tcInstSigTyVars, tcInstType, tcInstSigType,
24   tcSplitRhoTyM,
25
26   --------------------------------
27   -- Checking type validity
28   Rank, UserTypeCtxt(..), checkValidType, pprUserTypeCtxt,
29   SourceTyCtxt(..), checkValidTheta, 
30   checkValidInstHead, instTypeErr, checkAmbiguity,
31
32   --------------------------------
33   -- Zonking
34   zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkTcSigTyVars,
35   zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
36   zonkTcPredType, zonkTcTypeToType, zonkTcTyVarToTyVar, zonkKindEnv,
37
38   ) where
39
40 #include "HsVersions.h"
41
42
43 -- friends:
44 import TypeRep          ( Type(..), SourceType(..), TyNote(..),  -- Friend; can see representation
45                           Kind, ThetaType
46                         ) 
47 import TcType           ( TcType, TcThetaType, TcTauType, TcPredType,
48                           TcTyVarSet, TcKind, TcTyVar, TyVarDetails(..),
49                           tcEqType, tcCmpPred,
50                           tcSplitRhoTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe, 
51                           tcSplitTyConApp_maybe, tcSplitForAllTys,
52                           tcGetTyVar, tcIsTyVarTy, tcSplitSigmaTy, 
53                           isUnLiftedType, isIPPred, 
54
55                           mkAppTy, mkTyVarTy, mkTyVarTys, 
56                           tyVarsOfPred, getClassPredTys_maybe,
57
58                           liftedTypeKind, openTypeKind, defaultKind, superKind,
59                           superBoxity, liftedBoxity, typeKind,
60                           tyVarsOfType, tyVarsOfTypes, 
61                           eqKind, isTypeKind,
62
63                           isFFIArgumentTy, isFFIImportResultTy
64                         )
65 import Subst            ( Subst, mkTopTyVarSubst, substTy )
66 import Class            ( Class, classArity, className )
67 import TyCon            ( TyCon, mkPrimTyCon, isSynTyCon, isUnboxedTupleTyCon, 
68                           tyConArity, tyConName )
69 import PrimRep          ( PrimRep(VoidRep) )
70 import Var              ( TyVar, tyVarKind, tyVarName, isTyVar, mkTyVar, isMutTyVar )
71
72 -- others:
73 import TcMonad          -- TcType, amongst others
74 import TysWiredIn       ( voidTy )
75 import PrelNames        ( cCallableClassKey, cReturnableClassKey, hasKey )
76 import ForeignCall      ( Safety(..) )
77 import FunDeps          ( grow )
78 import PprType          ( pprPred, pprSourceType, pprTheta, pprClassPred )
79 import Name             ( Name, NamedThing(..), setNameUnique, mkSysLocalName,
80                           mkLocalName, mkDerivedTyConOcc
81                         )
82 import VarSet
83 import CmdLineOpts      ( dopt, DynFlag(..) )
84 import Unique           ( Uniquable(..) )
85 import SrcLoc           ( noSrcLoc )
86 import Util             ( nOfThem, isSingleton, equalLength )
87 import ListSetOps       ( removeDups )
88 import Outputable
89 \end{code}
90
91
92 %************************************************************************
93 %*                                                                      *
94 \subsection{New type variables}
95 %*                                                                      *
96 %************************************************************************
97
98 \begin{code}
99 newTyVar :: Kind -> NF_TcM TcTyVar
100 newTyVar kind
101   = tcGetUnique         `thenNF_Tc` \ uniq ->
102     tcNewMutTyVar (mkSysLocalName uniq SLIT("t")) kind VanillaTv
103
104 newTyVarTy  :: Kind -> NF_TcM TcType
105 newTyVarTy kind
106   = newTyVar kind       `thenNF_Tc` \ tc_tyvar ->
107     returnNF_Tc (TyVarTy tc_tyvar)
108
109 newHoleTyVarTy :: NF_TcM TcType
110   = tcGetUnique         `thenNF_Tc` \ uniq ->
111     tcNewMutTyVar (mkSysLocalName uniq SLIT("h")) openTypeKind HoleTv   `thenNF_Tc` \ tv ->
112     returnNF_Tc (TyVarTy tv)
113
114 newTyVarTys :: Int -> Kind -> NF_TcM [TcType]
115 newTyVarTys n kind = mapNF_Tc newTyVarTy (nOfThem n kind)
116
117 newKindVar :: NF_TcM TcKind
118 newKindVar
119   = tcGetUnique                                                         `thenNF_Tc` \ uniq ->
120     tcNewMutTyVar (mkSysLocalName uniq SLIT("k")) superKind VanillaTv   `thenNF_Tc` \ kv ->
121     returnNF_Tc (TyVarTy kv)
122
123 newKindVars :: Int -> NF_TcM [TcKind]
124 newKindVars n = mapNF_Tc (\ _ -> newKindVar) (nOfThem n ())
125
126 newBoxityVar :: NF_TcM TcKind
127 newBoxityVar
128   = tcGetUnique                                                           `thenNF_Tc` \ uniq ->
129     tcNewMutTyVar (mkSysLocalName uniq SLIT("bx")) superBoxity VanillaTv  `thenNF_Tc` \ kv ->
130     returnNF_Tc (TyVarTy kv)
131 \end{code}
132
133
134 %************************************************************************
135 %*                                                                      *
136 \subsection{Type instantiation}
137 %*                                                                      *
138 %************************************************************************
139
140 I don't understand why this is needed
141 An old comments says "No need for tcSplitForAllTyM because a type 
142         variable can't be instantiated to a for-all type"
143 But the same is true of rho types!
144
145 \begin{code}
146 tcSplitRhoTyM :: TcType -> NF_TcM (TcThetaType, TcType)
147 tcSplitRhoTyM t
148   = go t t []
149  where
150         -- A type variable is never instantiated to a dictionary type,
151         -- so we don't need to do a tcReadVar on the "arg".
152     go syn_t (FunTy arg res) ts = case tcSplitPredTy_maybe arg of
153                                         Just pair -> go res res (pair:ts)
154                                         Nothing   -> returnNF_Tc (reverse ts, syn_t)
155     go syn_t (NoteTy n t)    ts = go syn_t t ts
156     go syn_t (TyVarTy tv)    ts = getTcTyVar tv         `thenNF_Tc` \ maybe_ty ->
157                                   case maybe_ty of
158                                     Just ty | not (tcIsTyVarTy ty) -> go syn_t ty ts
159                                     other                          -> returnNF_Tc (reverse ts, syn_t)
160     go syn_t (UsageTy _ t)   ts = go syn_t t ts
161     go syn_t t               ts = returnNF_Tc (reverse ts, syn_t)
162 \end{code}
163
164
165 %************************************************************************
166 %*                                                                      *
167 \subsection{Type instantiation}
168 %*                                                                      *
169 %************************************************************************
170
171 Instantiating a bunch of type variables
172
173 \begin{code}
174 tcInstTyVars :: [TyVar] 
175              -> NF_TcM ([TcTyVar], [TcType], Subst)
176
177 tcInstTyVars tyvars
178   = mapNF_Tc tcInstTyVar tyvars `thenNF_Tc` \ tc_tyvars ->
179     let
180         tys = mkTyVarTys tc_tyvars
181     in
182     returnNF_Tc (tc_tyvars, tys, mkTopTyVarSubst tyvars tys)
183                 -- Since the tyvars are freshly made,
184                 -- they cannot possibly be captured by
185                 -- any existing for-alls.  Hence mkTopTyVarSubst
186
187 tcInstTyVar tyvar
188   = tcGetUnique                 `thenNF_Tc` \ uniq ->
189     let
190         name = setNameUnique (tyVarName tyvar) uniq
191         -- Note that we don't change the print-name
192         -- This won't confuse the type checker but there's a chance
193         -- that two different tyvars will print the same way 
194         -- in an error message.  -dppr-debug will show up the difference
195         -- Better watch out for this.  If worst comes to worst, just
196         -- use mkSysLocalName.
197     in
198     tcNewMutTyVar name (tyVarKind tyvar) VanillaTv
199
200 tcInstSigTyVars :: TyVarDetails -> [TyVar] -> NF_TcM [TcTyVar]
201 tcInstSigTyVars details tyvars  -- Very similar to tcInstTyVar
202   = tcGetUniques        `thenNF_Tc` \ uniqs ->
203     listTc [ ASSERT( not (kind `eqKind` openTypeKind) ) -- Shouldn't happen
204              tcNewMutTyVar name kind details
205            | (tyvar, uniq) <- tyvars `zip` uniqs,
206              let name = setNameUnique (tyVarName tyvar) uniq, 
207              let kind = tyVarKind tyvar
208            ]
209 \end{code}
210
211 @tcInstType@ instantiates the outer-level for-alls of a TcType with
212 fresh type variables, splits off the dictionary part, and returns the results.
213
214 \begin{code}
215 tcInstType :: TcType -> NF_TcM ([TcTyVar], TcThetaType, TcType)
216 tcInstType ty
217   = case tcSplitForAllTys ty of
218         ([],     rho) ->        -- There may be overloading but no type variables;
219                                 --      (?x :: Int) => Int -> Int
220                          let
221                            (theta, tau) = tcSplitRhoTy rho      -- Used to be tcSplitRhoTyM
222                          in
223                          returnNF_Tc ([], theta, tau)
224
225         (tyvars, rho) -> tcInstTyVars tyvars                    `thenNF_Tc` \ (tyvars', _, tenv)  ->
226                          let
227                            (theta, tau) = tcSplitRhoTy (substTy tenv rho)       -- Used to be tcSplitRhoTyM
228                          in
229                          returnNF_Tc (tyvars', theta, tau)
230
231
232 tcInstSigType :: TyVarDetails -> Type -> NF_TcM ([TcTyVar], TcThetaType, TcType)
233 -- Very similar to tcInstSigType, but uses signature type variables
234 -- Also, somewhat arbitrarily, don't deal with the monomorphic case so efficiently
235 tcInstSigType tv_details poly_ty
236  = let
237         (tyvars, rho) = tcSplitForAllTys poly_ty
238    in
239    tcInstSigTyVars tv_details tyvars            `thenNF_Tc` \ tyvars' ->
240         -- Make *signature* type variables
241
242    let
243      tyvar_tys' = mkTyVarTys tyvars'
244      rho' = substTy (mkTopTyVarSubst tyvars tyvar_tys') rho
245         -- mkTopTyVarSubst because the tyvars' are fresh
246
247      (theta', tau') = tcSplitRhoTy rho'
248         -- This splitRhoTy tries hard to make sure that tau' is a type synonym
249         -- wherever possible, which can improve interface files.
250    in
251    returnNF_Tc (tyvars', theta', tau')
252 \end{code}
253
254
255
256 %************************************************************************
257 %*                                                                      *
258 \subsection{Putting and getting  mutable type variables}
259 %*                                                                      *
260 %************************************************************************
261
262 \begin{code}
263 putTcTyVar :: TcTyVar -> TcType -> NF_TcM TcType
264 getTcTyVar :: TcTyVar -> NF_TcM (Maybe TcType)
265 \end{code}
266
267 Putting is easy:
268
269 \begin{code}
270 putTcTyVar tyvar ty 
271   | not (isMutTyVar tyvar)
272   = pprTrace "putTcTyVar" (ppr tyvar) $
273     returnNF_Tc ty
274
275   | otherwise
276   = ASSERT( isMutTyVar tyvar )
277     UASSERT2( not (isUTy ty), ppr tyvar <+> ppr ty )
278     tcWriteMutTyVar tyvar (Just ty)     `thenNF_Tc_`
279     returnNF_Tc ty
280 \end{code}
281
282 Getting is more interesting.  The easy thing to do is just to read, thus:
283
284 \begin{verbatim}
285 getTcTyVar tyvar = tcReadMutTyVar tyvar
286 \end{verbatim}
287
288 But it's more fun to short out indirections on the way: If this
289 version returns a TyVar, then that TyVar is unbound.  If it returns
290 any other type, then there might be bound TyVars embedded inside it.
291
292 We return Nothing iff the original box was unbound.
293
294 \begin{code}
295 getTcTyVar tyvar
296   | not (isMutTyVar tyvar)
297   = pprTrace "getTcTyVar" (ppr tyvar) $
298     returnNF_Tc (Just (mkTyVarTy tyvar))
299
300   | otherwise
301   = ASSERT2( isMutTyVar tyvar, ppr tyvar )
302     tcReadMutTyVar tyvar                                `thenNF_Tc` \ maybe_ty ->
303     case maybe_ty of
304         Just ty -> short_out ty                         `thenNF_Tc` \ ty' ->
305                    tcWriteMutTyVar tyvar (Just ty')     `thenNF_Tc_`
306                    returnNF_Tc (Just ty')
307
308         Nothing    -> returnNF_Tc Nothing
309
310 short_out :: TcType -> NF_TcM TcType
311 short_out ty@(TyVarTy tyvar)
312   | not (isMutTyVar tyvar)
313   = returnNF_Tc ty
314
315   | otherwise
316   = tcReadMutTyVar tyvar        `thenNF_Tc` \ maybe_ty ->
317     case maybe_ty of
318         Just ty' -> short_out ty'                       `thenNF_Tc` \ ty' ->
319                     tcWriteMutTyVar tyvar (Just ty')    `thenNF_Tc_`
320                     returnNF_Tc ty'
321
322         other    -> returnNF_Tc ty
323
324 short_out other_ty = returnNF_Tc other_ty
325 \end{code}
326
327
328 %************************************************************************
329 %*                                                                      *
330 \subsection{Zonking -- the exernal interfaces}
331 %*                                                                      *
332 %************************************************************************
333
334 -----------------  Type variables
335
336 \begin{code}
337 zonkTcTyVars :: [TcTyVar] -> NF_TcM [TcType]
338 zonkTcTyVars tyvars = mapNF_Tc zonkTcTyVar tyvars
339
340 zonkTcTyVarsAndFV :: [TcTyVar] -> NF_TcM TcTyVarSet
341 zonkTcTyVarsAndFV tyvars = mapNF_Tc zonkTcTyVar tyvars  `thenNF_Tc` \ tys ->
342                            returnNF_Tc (tyVarsOfTypes tys)
343
344 zonkTcTyVar :: TcTyVar -> NF_TcM TcType
345 zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnNF_Tc (TyVarTy tv)) tyvar
346
347 zonkTcSigTyVars :: [TcTyVar] -> NF_TcM [TcTyVar]
348 -- This guy is to zonk the tyvars we're about to feed into tcSimplify
349 -- Usually this job is done by checkSigTyVars, but in a couple of places
350 -- that is overkill, so we use this simpler chap
351 zonkTcSigTyVars tyvars
352   = zonkTcTyVars tyvars `thenNF_Tc` \ tys ->
353     returnNF_Tc (map (tcGetTyVar "zonkTcSigTyVars") tys)
354 \end{code}
355
356 -----------------  Types
357
358 \begin{code}
359 zonkTcType :: TcType -> NF_TcM TcType
360 zonkTcType ty = zonkType (\ tv -> returnNF_Tc (TyVarTy tv)) ty
361
362 zonkTcTypes :: [TcType] -> NF_TcM [TcType]
363 zonkTcTypes tys = mapNF_Tc zonkTcType tys
364
365 zonkTcClassConstraints cts = mapNF_Tc zonk cts
366     where zonk (clas, tys)
367             = zonkTcTypes tys   `thenNF_Tc` \ new_tys ->
368               returnNF_Tc (clas, new_tys)
369
370 zonkTcThetaType :: TcThetaType -> NF_TcM TcThetaType
371 zonkTcThetaType theta = mapNF_Tc zonkTcPredType theta
372
373 zonkTcPredType :: TcPredType -> NF_TcM TcPredType
374 zonkTcPredType (ClassP c ts)
375   = zonkTcTypes ts      `thenNF_Tc` \ new_ts ->
376     returnNF_Tc (ClassP c new_ts)
377 zonkTcPredType (IParam n t)
378   = zonkTcType t        `thenNF_Tc` \ new_t ->
379     returnNF_Tc (IParam n new_t)
380 \end{code}
381
382 -------------------  These ...ToType, ...ToKind versions
383                      are used at the end of type checking
384
385 \begin{code}
386 zonkKindEnv :: [(Name, TcKind)] -> NF_TcM [(Name, Kind)]
387 zonkKindEnv pairs 
388   = mapNF_Tc zonk_it pairs
389  where
390     zonk_it (name, tc_kind) = zonkType zonk_unbound_kind_var tc_kind `thenNF_Tc` \ kind ->
391                               returnNF_Tc (name, kind)
392
393         -- When zonking a kind, we want to
394         --      zonk a *kind* variable to (Type *)
395         --      zonk a *boxity* variable to *
396     zonk_unbound_kind_var kv | tyVarKind kv `eqKind` superKind   = putTcTyVar kv liftedTypeKind
397                              | tyVarKind kv `eqKind` superBoxity = putTcTyVar kv liftedBoxity
398                              | otherwise                         = pprPanic "zonkKindEnv" (ppr kv)
399                         
400 zonkTcTypeToType :: TcType -> NF_TcM Type
401 zonkTcTypeToType ty = zonkType zonk_unbound_tyvar ty
402   where
403         -- Zonk a mutable but unbound type variable to
404         --      Void            if it has kind Lifted
405         --      :Void           otherwise
406         -- We know it's unbound even though we don't carry an environment,
407         -- because at the binding site for a type variable we bind the
408         -- mutable tyvar to a fresh immutable one.  So the mutable store
409         -- plays the role of an environment.  If we come across a mutable
410         -- type variable that isn't so bound, it must be completely free.
411     zonk_unbound_tyvar tv
412         | kind `eqKind` liftedTypeKind || kind `eqKind` openTypeKind
413         = putTcTyVar tv voidTy  -- Just to avoid creating a new tycon in
414                                 -- this vastly common case
415         | otherwise
416         = putTcTyVar tv (TyConApp (mk_void_tycon tv kind) [])
417         where
418           kind = tyVarKind tv
419
420     mk_void_tycon tv kind       -- Make a new TyCon with the same kind as the 
421                                 -- type variable tv.  Same name too, apart from
422                                 -- making it start with a colon (sigh)
423                 -- I dread to think what will happen if this gets out into an 
424                 -- interface file.  Catastrophe likely.  Major sigh.
425         = pprTrace "Urk! Inventing strangely-kinded void TyCon" (ppr tc_name) $
426           mkPrimTyCon tc_name kind 0 [] VoidRep
427         where
428           tc_name = mkLocalName (getUnique tv) (mkDerivedTyConOcc (getOccName tv)) noSrcLoc
429
430 -- zonkTcTyVarToTyVar is applied to the *binding* occurrence 
431 -- of a type variable, at the *end* of type checking.  It changes
432 -- the *mutable* type variable into an *immutable* one.
433 -- 
434 -- It does this by making an immutable version of tv and binds tv to it.
435 -- Now any bound occurences of the original type variable will get 
436 -- zonked to the immutable version.
437
438 zonkTcTyVarToTyVar :: TcTyVar -> NF_TcM TyVar
439 zonkTcTyVarToTyVar tv
440   = let
441                 -- Make an immutable version, defaulting 
442                 -- the kind to lifted if necessary
443         immut_tv    = mkTyVar (tyVarName tv) (defaultKind (tyVarKind tv))
444         immut_tv_ty = mkTyVarTy immut_tv
445
446         zap tv = putTcTyVar tv immut_tv_ty
447                 -- Bind the mutable version to the immutable one
448     in 
449         -- If the type variable is mutable, then bind it to immut_tv_ty
450         -- so that all other occurrences of the tyvar will get zapped too
451     zonkTyVar zap tv            `thenNF_Tc` \ ty2 ->
452
453     WARN( not (immut_tv_ty `tcEqType` ty2), ppr tv $$ ppr immut_tv $$ ppr ty2 )
454
455     returnNF_Tc immut_tv
456 \end{code}
457
458
459 %************************************************************************
460 %*                                                                      *
461 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
462 %*                                                                      *
463 %*              For internal use only!                                  *
464 %*                                                                      *
465 %************************************************************************
466
467 \begin{code}
468 -- zonkType is used for Kinds as well
469
470 -- For unbound, mutable tyvars, zonkType uses the function given to it
471 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
472 --      type variable and zonks the kind too
473
474 zonkType :: (TcTyVar -> NF_TcM Type)    -- What to do with unbound mutable type variables
475                                         -- see zonkTcType, and zonkTcTypeToType
476          -> TcType
477          -> NF_TcM Type
478 zonkType unbound_var_fn ty
479   = go ty
480   where
481     go (TyConApp tycon tys)       = mapNF_Tc go tys     `thenNF_Tc` \ tys' ->
482                                     returnNF_Tc (TyConApp tycon tys')
483
484     go (NoteTy (SynNote ty1) ty2) = go ty1              `thenNF_Tc` \ ty1' ->
485                                     go ty2              `thenNF_Tc` \ ty2' ->
486                                     returnNF_Tc (NoteTy (SynNote ty1') ty2')
487
488     go (NoteTy (FTVNote _) ty2)   = go ty2      -- Discard free-tyvar annotations
489
490     go (SourceTy p)               = go_pred p           `thenNF_Tc` \ p' ->
491                                     returnNF_Tc (SourceTy p')
492
493     go (FunTy arg res)            = go arg              `thenNF_Tc` \ arg' ->
494                                     go res              `thenNF_Tc` \ res' ->
495                                     returnNF_Tc (FunTy arg' res')
496  
497     go (AppTy fun arg)            = go fun              `thenNF_Tc` \ fun' ->
498                                     go arg              `thenNF_Tc` \ arg' ->
499                                     returnNF_Tc (mkAppTy fun' arg')
500
501     go (UsageTy u ty)             = go u                `thenNF_Tc` \ u'  ->
502                                     go ty               `thenNF_Tc` \ ty' ->
503                                     returnNF_Tc (UsageTy u' ty')
504
505         -- The two interesting cases!
506     go (TyVarTy tyvar)     = zonkTyVar unbound_var_fn tyvar
507
508     go (ForAllTy tyvar ty) = zonkTcTyVarToTyVar tyvar   `thenNF_Tc` \ tyvar' ->
509                              go ty                      `thenNF_Tc` \ ty' ->
510                              returnNF_Tc (ForAllTy tyvar' ty')
511
512     go_pred (ClassP c tys) = mapNF_Tc go tys    `thenNF_Tc` \ tys' ->
513                              returnNF_Tc (ClassP c tys')
514     go_pred (NType tc tys) = mapNF_Tc go tys    `thenNF_Tc` \ tys' ->
515                              returnNF_Tc (NType tc tys')
516     go_pred (IParam n ty)  = go ty              `thenNF_Tc` \ ty' ->
517                              returnNF_Tc (IParam n ty')
518
519 zonkTyVar :: (TcTyVar -> NF_TcM Type)           -- What to do for an unbound mutable variable
520           -> TcTyVar -> NF_TcM TcType
521 zonkTyVar unbound_var_fn tyvar 
522   | not (isMutTyVar tyvar)      -- Not a mutable tyvar.  This can happen when
523                                 -- zonking a forall type, when the bound type variable
524                                 -- needn't be mutable
525   = ASSERT( isTyVar tyvar )             -- Should not be any immutable kind vars
526     returnNF_Tc (TyVarTy tyvar)
527
528   | otherwise
529   =  getTcTyVar tyvar   `thenNF_Tc` \ maybe_ty ->
530      case maybe_ty of
531           Nothing       -> unbound_var_fn tyvar                 -- Mutable and unbound
532           Just other_ty -> zonkType unbound_var_fn other_ty     -- Bound
533 \end{code}
534
535
536
537 %************************************************************************
538 %*                                                                      *
539 \subsection{Checking a user type}
540 %*                                                                      *
541 %************************************************************************
542
543 When dealing with a user-written type, we first translate it from an HsType
544 to a Type, performing kind checking, and then check various things that should 
545 be true about it.  We don't want to perform these checks at the same time
546 as the initial translation because (a) they are unnecessary for interface-file
547 types and (b) when checking a mutually recursive group of type and class decls,
548 we can't "look" at the tycons/classes yet.  Also, the checks are are rather
549 diverse, and used to really mess up the other code.
550
551 One thing we check for is 'rank'.  
552
553         Rank 0:         monotypes (no foralls)
554         Rank 1:         foralls at the front only, Rank 0 inside
555         Rank 2:         foralls at the front, Rank 1 on left of fn arrow,
556
557         basic ::= tyvar | T basic ... basic
558
559         r2  ::= forall tvs. cxt => r2a
560         r2a ::= r1 -> r2a | basic
561         r1  ::= forall tvs. cxt => r0
562         r0  ::= r0 -> r0 | basic
563         
564 Another thing is to check that type synonyms are saturated. 
565 This might not necessarily show up in kind checking.
566         type A i = i
567         data T k = MkT (k Int)
568         f :: T A        -- BAD!
569
570         
571 \begin{code}
572 data UserTypeCtxt 
573   = FunSigCtxt Name     -- Function type signature
574   | ExprSigCtxt         -- Expression type signature
575   | ConArgCtxt Name     -- Data constructor argument
576   | TySynCtxt Name      -- RHS of a type synonym decl
577   | GenPatCtxt          -- Pattern in generic decl
578                         --      f{| a+b |} (Inl x) = ...
579   | PatSigCtxt          -- Type sig in pattern
580                         --      f (x::t) = ...
581   | ResSigCtxt          -- Result type sig
582                         --      f x :: t = ....
583   | ForSigCtxt Name     -- Foreign inport or export signature
584   | RuleSigCtxt Name    -- Signature on a forall'd variable in a RULE
585
586 -- Notes re TySynCtxt
587 -- We allow type synonyms that aren't types; e.g.  type List = []
588 --
589 -- If the RHS mentions tyvars that aren't in scope, we'll 
590 -- quantify over them:
591 --      e.g.    type T = a->a
592 -- will become  type T = forall a. a->a
593 --
594 -- With gla-exts that's right, but for H98 we should complain. 
595
596
597 pprUserTypeCtxt (FunSigCtxt n)  = ptext SLIT("the type signature for") <+> quotes (ppr n)
598 pprUserTypeCtxt ExprSigCtxt     = ptext SLIT("an expression type signature")
599 pprUserTypeCtxt (ConArgCtxt c)  = ptext SLIT("the type of constructor") <+> quotes (ppr c)
600 pprUserTypeCtxt (TySynCtxt c)   = ptext SLIT("the RHS of a type synonym declaration") <+> quotes (ppr c)
601 pprUserTypeCtxt GenPatCtxt      = ptext SLIT("the type pattern of a generic definition")
602 pprUserTypeCtxt PatSigCtxt      = ptext SLIT("a pattern type signature")
603 pprUserTypeCtxt ResSigCtxt      = ptext SLIT("a result type signature")
604 pprUserTypeCtxt (ForSigCtxt n)  = ptext SLIT("the foreign signature for") <+> quotes (ppr n)
605 pprUserTypeCtxt (RuleSigCtxt n) = ptext SLIT("the type signature on") <+> quotes (ppr n)
606 \end{code}
607
608 \begin{code}
609 checkValidType :: UserTypeCtxt -> Type -> TcM ()
610 -- Checks that the type is valid for the given context
611 checkValidType ctxt ty
612   = doptsTc Opt_GlasgowExts     `thenNF_Tc` \ gla_exts ->
613     let 
614         rank | gla_exts = Arbitrary
615              | otherwise
616              = case ctxt of     -- Haskell 98
617                  GenPatCtxt     -> Rank 0
618                  PatSigCtxt     -> Rank 0
619                  ResSigCtxt     -> Rank 0
620                  TySynCtxt _    -> Rank 0
621                  ExprSigCtxt    -> Rank 1
622                  FunSigCtxt _   -> Rank 1
623                  ConArgCtxt _   -> Rank 1       -- We are given the type of the entire
624                                                 -- constructor, hence rank 1
625                  ForSigCtxt _   -> Rank 1
626                  RuleSigCtxt _  -> Rank 1
627
628         actual_kind = typeKind ty
629
630         actual_kind_is_lifted = actual_kind `eqKind` liftedTypeKind
631
632         kind_ok = case ctxt of
633                         TySynCtxt _  -> True    -- Any kind will do
634                         GenPatCtxt   -> actual_kind_is_lifted
635                         ForSigCtxt _ -> actual_kind_is_lifted
636                         other        -> isTypeKind actual_kind
637     in
638     tcAddErrCtxt (checkTypeCtxt ctxt ty)        $
639
640         -- Check that the thing has kind Type, and is lifted if necessary
641     checkTc kind_ok (kindErr actual_kind)       `thenTc_`
642
643         -- Check the internal validity of the type itself
644     check_poly_type rank ty
645
646
647 checkTypeCtxt ctxt ty
648   = vcat [ptext SLIT("In the type:") <+> ppr_ty ty,
649           ptext SLIT("While checking") <+> pprUserTypeCtxt ctxt ]
650
651         -- Hack alert.  If there are no tyvars, (ppr sigma_ty) will print
652         -- something strange like {Eq k} -> k -> k, because there is no
653         -- ForAll at the top of the type.  Since this is going to the user
654         -- we want it to look like a proper Haskell type even then; hence the hack
655         -- 
656         -- This shows up in the complaint about
657         --      case C a where
658         --        op :: Eq a => a -> a
659 ppr_ty ty | null forall_tvs && not (null theta) = pprTheta theta <+> ptext SLIT("=>") <+> ppr tau
660           | otherwise                        = ppr ty
661           where
662             (forall_tvs, theta, tau) = tcSplitSigmaTy ty
663 \end{code}
664
665
666 \begin{code}
667 data Rank = Rank Int | Arbitrary
668
669 decRank :: Rank -> Rank
670 decRank Arbitrary = Arbitrary
671 decRank (Rank n)  = Rank (n-1)
672
673 check_poly_type :: Rank -> Type -> TcM ()
674 check_poly_type (Rank 0) ty 
675   = check_tau_type (Rank 0) False ty
676
677 check_poly_type rank ty 
678   = let
679         (tvs, theta, tau) = tcSplitSigmaTy ty
680     in
681     check_valid_theta SigmaCtxt theta           `thenTc_`
682     check_tau_type (decRank rank) False tau     `thenTc_`
683     checkFreeness tvs theta                     `thenTc_`
684     checkAmbiguity tvs theta (tyVarsOfType tau)
685
686 ----------------------------------------
687 check_arg_type :: Type -> TcM ()
688 -- The sort of type that can instantiate a type variable,
689 -- or be the argument of a type constructor.
690 -- Not an unboxed tuple, not a forall.
691 -- Other unboxed types are very occasionally allowed as type
692 -- arguments depending on the kind of the type constructor
693 -- 
694 -- For example, we want to reject things like:
695 --
696 --      instance Ord a => Ord (forall s. T s a)
697 -- and
698 --      g :: T s (forall b.b)
699 --
700 -- NB: unboxed tuples can have polymorphic or unboxed args.
701 --     This happens in the workers for functions returning
702 --     product types with polymorphic components.
703 --     But not in user code
704 -- 
705 -- Question: what about nested unboxed tuples?
706 --           Currently rejected.
707 check_arg_type ty 
708   = check_tau_type (Rank 0) False ty    `thenTc_` 
709     checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
710
711 ----------------------------------------
712 check_tau_type :: Rank -> Bool -> Type -> TcM ()
713 -- Rank is allowed rank for function args
714 -- No foralls otherwise
715 -- Bool is True iff unboxed tuple are allowed here
716
717 check_tau_type rank ubx_tup_ok ty@(UsageTy _ _)  = failWithTc (usageTyErr ty)
718 check_tau_type rank ubx_tup_ok ty@(ForAllTy _ _) = failWithTc (forAllTyErr ty)
719 check_tau_type rank ubx_tup_ok (SourceTy sty)    = getDOptsTc           `thenNF_Tc` \ dflags ->
720                                                    check_source_ty dflags TypeCtxt sty
721 check_tau_type rank ubx_tup_ok (TyVarTy _)       = returnTc ()
722 check_tau_type rank ubx_tup_ok ty@(FunTy arg_ty res_ty)
723   = check_poly_type rank      arg_ty    `thenTc_`
724     check_tau_type  rank True res_ty
725
726 check_tau_type rank ubx_tup_ok (AppTy ty1 ty2)
727   = check_arg_type ty1 `thenTc_` check_arg_type ty2
728
729 check_tau_type rank ubx_tup_ok (NoteTy note ty)
730   = check_note note `thenTc_` check_tau_type rank ubx_tup_ok ty
731
732 check_tau_type rank ubx_tup_ok ty@(TyConApp tc tys)
733   | isSynTyCon tc
734   = checkTc syn_arity_ok arity_msg      `thenTc_`
735     mapTc_ check_arg_type tys
736     
737   | isUnboxedTupleTyCon tc
738   = checkTc ubx_tup_ok ubx_tup_msg      `thenTc_`
739     mapTc_ (check_tau_type (Rank 0) True) tys   -- Args are allowed to be unlifted, or
740                                                 -- more unboxed tuples, so can't use check_arg_ty
741
742   | otherwise
743   = mapTc_ check_arg_type tys
744
745   where
746     syn_arity_ok = tc_arity <= n_args
747                 -- It's OK to have an *over-applied* type synonym
748                 --      data Tree a b = ...
749                 --      type Foo a = Tree [a]
750                 --      f :: Foo a b -> ...
751     n_args    = length tys
752     tc_arity  = tyConArity tc
753
754     arity_msg   = arityErr "Type synonym" (tyConName tc) tc_arity n_args
755     ubx_tup_msg = ubxArgTyErr ty
756
757 ----------------------------------------
758 check_note (FTVNote _)  = returnTc ()
759 check_note (SynNote ty) = check_tau_type (Rank 0) False ty
760
761 ----------------------------------------
762 forAllTyErr     ty = ptext SLIT("Illegal polymorphic type:") <+> ppr_ty ty
763 usageTyErr      ty = ptext SLIT("Illegal usage type:") <+> ppr_ty ty
764 unliftedArgErr  ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr_ty ty
765 ubxArgTyErr     ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr_ty ty
766 kindErr kind       = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
767 \end{code}
768
769 Check for ambiguity
770 ~~~~~~~~~~~~~~~~~~~
771           forall V. P => tau
772 is ambiguous if P contains generic variables
773 (i.e. one of the Vs) that are not mentioned in tau
774
775 However, we need to take account of functional dependencies
776 when we speak of 'mentioned in tau'.  Example:
777         class C a b | a -> b where ...
778 Then the type
779         forall x y. (C x y) => x
780 is not ambiguous because x is mentioned and x determines y
781
782 NB; the ambiguity check is only used for *user* types, not for types
783 coming from inteface files.  The latter can legitimately have
784 ambiguous types. Example
785
786    class S a where s :: a -> (Int,Int)
787    instance S Char where s _ = (1,1)
788    f:: S a => [a] -> Int -> (Int,Int)
789    f (_::[a]) x = (a*x,b)
790         where (a,b) = s (undefined::a)
791
792 Here the worker for f gets the type
793         fw :: forall a. S a => Int -> (# Int, Int #)
794
795 If the list of tv_names is empty, we have a monotype, and then we
796 don't need to check for ambiguity either, because the test can't fail
797 (see is_ambig).
798
799 \begin{code}
800 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
801 checkAmbiguity forall_tyvars theta tau_tyvars
802   = mapTc_ complain (filter is_ambig theta)
803   where
804     complain pred     = addErrTc (ambigErr pred)
805     extended_tau_vars = grow theta tau_tyvars
806     is_ambig pred     = any ambig_var (varSetElems (tyVarsOfPred pred))
807
808     ambig_var ct_var  = (ct_var `elem` forall_tyvars) &&
809                         not (ct_var `elemVarSet` extended_tau_vars)
810
811     is_free ct_var    = not (ct_var `elem` forall_tyvars)
812
813 ambigErr pred
814   = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
815          nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
816                  ptext SLIT("must be reachable from the type after the '=>'"))]
817 \end{code}
818     
819 In addition, GHC insists that at least one type variable
820 in each constraint is in V.  So we disallow a type like
821         forall a. Eq b => b -> b
822 even in a scope where b is in scope.
823
824 \begin{code}
825 checkFreeness forall_tyvars theta
826   = mapTc_ complain (filter is_free theta)
827   where    
828     is_free pred     =  not (isIPPred pred)
829                      && not (any bound_var (varSetElems (tyVarsOfPred pred)))
830     bound_var ct_var = ct_var `elem` forall_tyvars
831     complain pred    = addErrTc (freeErr pred)
832
833 freeErr pred
834   = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
835                    ptext SLIT("are already in scope"),
836          nest 4 (ptext SLIT("At least one must be universally quantified here"))
837     ]
838 \end{code}
839
840
841 %************************************************************************
842 %*                                                                      *
843 \subsection{Checking a theta or source type}
844 %*                                                                      *
845 %************************************************************************
846
847 \begin{code}
848 data SourceTyCtxt
849   = ClassSCCtxt Name    -- Superclasses of clas
850   | SigmaCtxt           -- Context of a normal for-all type
851   | DataTyCtxt Name     -- Context of a data decl
852   | TypeCtxt            -- Source type in an ordinary type
853   | InstThetaCtxt       -- Context of an instance decl
854   | InstHeadCtxt        -- Head of an instance decl
855                 
856 pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c)
857 pprSourceTyCtxt SigmaCtxt       = ptext SLIT("the context of a polymorphic type")
858 pprSourceTyCtxt (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc)
859 pprSourceTyCtxt InstThetaCtxt   = ptext SLIT("the context of an instance declaration")
860 pprSourceTyCtxt InstHeadCtxt    = ptext SLIT("the head of an instance declaration")
861 pprSourceTyCtxt TypeCtxt        = ptext SLIT("the context of a type")
862 \end{code}
863
864 \begin{code}
865 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
866 checkValidTheta ctxt theta 
867   = tcAddErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
868
869 -------------------------
870 check_valid_theta ctxt []
871   = returnTc ()
872 check_valid_theta ctxt theta
873   = getDOptsTc                                  `thenNF_Tc` \ dflags ->
874     warnTc (not (null dups)) (dupPredWarn dups) `thenNF_Tc_`
875     mapTc_ (check_source_ty dflags ctxt) theta
876   where
877     (_,dups) = removeDups tcCmpPred theta
878
879 -------------------------
880 check_source_ty dflags ctxt pred@(ClassP cls tys)
881   =     -- Class predicates are valid in all contexts
882     mapTc_ check_arg_type tys                   `thenTc_`
883     checkTc (arity == n_tys) arity_err          `thenTc_`
884     checkTc (all tyvar_head tys || arby_preds_ok)
885             (predTyVarErr pred $$ how_to_allow)
886
887   where
888     class_name = className cls
889     arity      = classArity cls
890     n_tys      = length tys
891     arity_err  = arityErr "Class" class_name arity n_tys
892
893     arby_preds_ok = case ctxt of
894                         InstHeadCtxt  -> True   -- We check for instance-head formation
895                                                 -- in checkValidInstHead
896                         InstThetaCtxt -> dopt Opt_AllowUndecidableInstances dflags
897                         other         -> dopt Opt_GlasgowExts               dflags
898
899     how_to_allow = case ctxt of
900                      InstHeadCtxt  -> empty     -- Should not happen
901                      InstThetaCtxt -> parens undecidableMsg
902                      other         -> parens (ptext SLIT("Use -fglasgow-exts to permit this"))
903
904 check_source_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
905         -- Implicit parameters only allows in type
906         -- signatures; not in instance decls, superclasses etc
907         -- The reason for not allowing implicit params in instances is a bit subtle
908         -- If we allowed        instance (?x::Int, Eq a) => Foo [a] where ...
909         -- then when we saw (e :: (?x::Int) => t) it would be unclear how to 
910         -- discharge all the potential usas of the ?x in e.   For example, a
911         -- constraint Foo [Int] might come out of e,and applying the
912         -- instance decl would show up two uses of ?x.
913
914 check_source_ty dflags TypeCtxt  (NType tc tys)   = mapTc_ check_arg_type tys
915
916 -- Catch-all
917 check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty)
918
919 -------------------------
920 tyvar_head ty                   -- Haskell 98 allows predicates of form 
921   | tcIsTyVarTy ty = True       --      C (a ty1 .. tyn)
922   | otherwise                   -- where a is a type variable
923   = case tcSplitAppTy_maybe ty of
924         Just (ty, _) -> tyvar_head ty
925         Nothing      -> False
926 \end{code}
927
928 \begin{code}
929 badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprSourceType sty
930 predTyVarErr pred  = ptext SLIT("Non-type variables in constraint:") <+> pprPred pred
931 dupPredWarn dups   = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
932
933 checkThetaCtxt ctxt theta
934   = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
935           ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
936 \end{code}
937
938
939 %************************************************************************
940 %*                                                                      *
941 \subsection{Checking for a decent instance head type}
942 %*                                                                      *
943 %************************************************************************
944
945 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
946 it must normally look like: @instance Foo (Tycon a b c ...) ...@
947
948 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
949 flag is on, or (2)~the instance is imported (they must have been
950 compiled elsewhere). In these cases, we let them go through anyway.
951
952 We can also have instances for functions: @instance Foo (a -> b) ...@.
953
954 \begin{code}
955 checkValidInstHead :: Type -> TcM (Class, [TcType])
956
957 checkValidInstHead ty   -- Should be a source type
958   = case tcSplitPredTy_maybe ty of {
959         Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
960         Just pred -> 
961
962     case getClassPredTys_maybe pred of {
963         Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
964         Just (clas,tys) ->
965
966     getDOptsTc                                  `thenNF_Tc` \ dflags ->
967     mapTc_ check_arg_type tys                   `thenTc_`
968     check_inst_head dflags clas tys             `thenTc_`
969     returnTc (clas, tys)
970     }}
971
972 check_inst_head dflags clas tys
973   |     -- CCALL CHECK
974         -- A user declaration of a CCallable/CReturnable instance
975         -- must be for a "boxed primitive" type.
976         (clas `hasKey` cCallableClassKey   
977             && not (ccallable_type first_ty)) 
978   ||    (clas `hasKey` cReturnableClassKey 
979             && not (creturnable_type first_ty))
980   = failWithTc (nonBoxedPrimCCallErr clas first_ty)
981
982         -- If GlasgowExts then check at least one isn't a type variable
983   | dopt Opt_GlasgowExts dflags
984   = check_tyvars dflags clas tys
985
986         -- WITH HASKELL 1.4, MUST HAVE C (T a b c)
987   | isSingleton tys,
988     Just (tycon, arg_tys) <- tcSplitTyConApp_maybe first_ty,
989     not (isSynTyCon tycon),             -- ...but not a synonym
990     all tcIsTyVarTy arg_tys,            -- Applied to type variables
991     equalLength (varSetElems (tyVarsOfTypes arg_tys)) arg_tys
992           -- This last condition checks that all the type variables are distinct
993   = returnTc ()
994
995   | otherwise
996   = failWithTc (instTypeErr (pprClassPred clas tys) head_shape_msg)
997
998   where
999     (first_ty : _)       = tys
1000
1001     ccallable_type   ty = isFFIArgumentTy dflags PlayRisky ty
1002     creturnable_type ty = isFFIImportResultTy dflags ty
1003         
1004     head_shape_msg = parens (text "The instance type must be of form (T a b c)" $$
1005                              text "where T is not a synonym, and a,b,c are distinct type variables")
1006
1007 check_tyvars dflags clas tys
1008         -- Check that at least one isn't a type variable
1009         -- unless -fallow-undecideable-instances
1010   | dopt Opt_AllowUndecidableInstances dflags = returnTc ()
1011   | not (all tcIsTyVarTy tys)                 = returnTc ()
1012   | otherwise                                 = failWithTc (instTypeErr (pprClassPred clas tys) msg)
1013   where
1014     msg =  parens (ptext SLIT("There must be at least one non-type-variable in the instance head")
1015                    $$ undecidableMsg)
1016
1017 undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this")
1018 \end{code}
1019
1020 \begin{code}
1021 instTypeErr pp_ty msg
1022   = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty, 
1023          nest 4 msg]
1024
1025 nonBoxedPrimCCallErr clas inst_ty
1026   = hang (ptext SLIT("Unacceptable instance type for ccall-ish class"))
1027          4 (pprClassPred clas [inst_ty])
1028 \end{code}
1029
1030