TcMType.lhs 64.7 KB
Newer Older
1
%
2
% (c) The University of Glasgow 2006
3 4 5
% (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
%

6 7 8 9
Monadic type operations

This module contains monadic operations over types that contain
mutable type variables
10 11

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

19
module TcMType (
20
  TcTyVar, TcKind, TcType, TcTauType, TcThetaType, TcTyVarSet,
21 22 23

  --------------------------------
  -- Creating new mutable type variables
24
  newFlexiTyVar,
25 26
  newFlexiTyVarTy,		-- Kind -> TcM TcType
  newFlexiTyVarTys,		-- Int -> Kind -> TcM [TcType]
dreixel's avatar
dreixel committed
27
  newMetaKindVar, newMetaKindVars,
28
  mkTcTyVarName,
29

30 31
  newMetaTyVar, readMetaTyVar, writeMetaTyVar, writeMetaTyVarRef,
  isFilledMetaTyVar, isFlexiMetaTyVar,
32 33

  --------------------------------
34
  -- Creating new evidence variables
batterseapower's avatar
batterseapower committed
35 36
  newEvVar, newEvVars,
  newEq, newIP, newDict,
37

38
  newWantedEvVar, newWantedEvVars,
39
  newTcEvBinds, addTcEvBind,
40

41 42
  --------------------------------
  -- Instantiation
Simon Peyton Jones's avatar
Simon Peyton Jones committed
43 44
  tcInstTyVars, tcInstSigTyVars,
  tcInstType, 
45 46 47
  tcInstSkolTyVars, tcInstSuperSkolTyVars,
  tcInstSkolTyVarsX, tcInstSuperSkolTyVarsX,
  tcInstSkolTyVar, tcInstSkolType,
48
  tcSkolDFunType, tcSuperSkolTyVars,
49

50 51
  --------------------------------
  -- Checking type validity
52
  Rank, UserTypeCtxt(..), checkValidType, checkValidMonoType,
53
  expectedKindInCtxt, 
dreixel's avatar
dreixel committed
54
  checkValidTheta, 
55
  checkValidInstHead, checkValidInstance, validDerivPred,
56
  checkInstTermination, checkValidFamInst, checkTyFamFreeness, 
57
  arityErr, 
58
  growPredTyVars, growThetaTyVars, 
59

60 61
  --------------------------------
  -- Zonking
dreixel's avatar
dreixel committed
62
  zonkType, zonkKind, zonkTcPredType, 
63
  zonkTcTypeCarefully, skolemiseUnboundMetaTyVar,
64
  zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkSigTyVar,
65
  zonkQuantifiedTyVar, zonkQuantifiedTyVars,
Ian Lynagh's avatar
Ian Lynagh committed
66
  zonkTcType, zonkTcTypes, zonkTcThetaType,
67 68 69 70

  zonkTcKind, defaultKindVarToStar, zonkCt, zonkCts,
  zonkImplication, zonkEvVar, zonkWantedEvVar,

71
  zonkWC, zonkWantedEvVars,
72
  zonkTcTypeAndSubst,
73
  tcGetGlobalTyVars, 
74

dreixel's avatar
dreixel committed
75
  compatKindTcM, isSubKindTcM
76 77 78 79 80
  ) where

#include "HsVersions.h"

-- friends:
81 82 83
import TypeRep
import TcType
import Type
dreixel's avatar
dreixel committed
84
import Kind
85 86 87
import Class
import TyCon
import Var
88 89

-- others:
90 91
import HsSyn		-- HsType
import TcRnMonad        -- TcType, amongst others
batterseapower's avatar
batterseapower committed
92
import IParam
93
import Id
94 95
import FunDeps
import Name
96
import VarSet
97
import ErrUtils
98 99
import DynFlags
import Util
100
import Maybes
101
import ListSetOps
102
import BasicTypes
103
import SrcLoc
104
import Outputable
105
import FastString
106
import Unique( Unique )
107
import Bag
108

Ian Lynagh's avatar
Ian Lynagh committed
109
import Control.Monad
110
import Data.List        ( (\\), partition, mapAccumL )
111 112 113 114 115
\end{code}


%************************************************************************
%*									*
116
	Kind variables
117 118 119 120
%*									*
%************************************************************************

\begin{code}
dreixel's avatar
dreixel committed
121 122
newMetaKindVar :: TcM TcKind
newMetaKindVar = do	{ uniq <- newUnique
123
		; ref <- newMutVar Flexi
dreixel's avatar
dreixel committed
124
		; return (mkTyVarTy (mkMetaKindVar uniq ref)) }
125

dreixel's avatar
dreixel committed
126 127
newMetaKindVars :: Int -> TcM [TcKind]
newMetaKindVars n = mapM (\ _ -> newMetaKindVar) (nOfThem n ())
128
\end{code}
129 130


131 132
%************************************************************************
%*									*
133
     Evidence variables; range over constraints we can abstract over
134 135 136 137
%*									*
%************************************************************************

\begin{code}
138 139 140 141
newEvVars :: TcThetaType -> TcM [EvVar]
newEvVars theta = mapM newEvVar theta

newWantedEvVar :: TcPredType -> TcM EvVar 
batterseapower's avatar
batterseapower committed
142
newWantedEvVar = newEvVar
143 144 145 146

newWantedEvVars :: TcThetaType -> TcM [EvVar] 
newWantedEvVars theta = mapM newWantedEvVar theta 

147
--------------
batterseapower's avatar
batterseapower committed
148

149 150
newEvVar :: TcPredType -> TcM EvVar
-- Creates new *rigid* variables for predicates
batterseapower's avatar
batterseapower committed
151 152
newEvVar ty = do { name <- newName (predTypeOccName ty) 
                 ; return (mkLocalId name ty) }
153

batterseapower's avatar
batterseapower committed
154 155 156 157
newEq :: TcType -> TcType -> TcM EvVar
newEq ty1 ty2
  = do { name <- newName (mkVarOccFS (fsLit "cobox"))
       ; return (mkLocalId name (mkEqPred (ty1, ty2))) }
158 159 160

newIP :: IPName Name -> TcType -> TcM IpId
newIP ip ty
batterseapower's avatar
batterseapower committed
161 162
  = do 	{ name <- newName (mkVarOccFS (ipFastString ip))
        ; return (mkLocalId name (mkIPPred ip ty)) }
163 164 165 166

newDict :: Class -> [TcType] -> TcM DictId
newDict cls tys 
  = do { name <- newName (mkDictOcc (getOccName cls))
batterseapower's avatar
batterseapower committed
167 168 169
       ; return (mkLocalId name (mkClassPred cls tys)) }

predTypeOccName :: PredType -> OccName
170
predTypeOccName ty = case classifyPredType ty of
batterseapower's avatar
batterseapower committed
171 172 173 174 175
    ClassPred cls _ -> mkDictOcc (getOccName cls)
    IPPred ip _     -> mkVarOccFS (ipFastString ip)
    EqPred _ _      -> mkVarOccFS (fsLit "cobox")
    TuplePred _     -> mkVarOccFS (fsLit "tup")
    IrredPred _     -> mkVarOccFS (fsLit "irred")
176 177 178
\end{code}


179 180
%************************************************************************
%*									*
181
	SkolemTvs (immutable)
182 183
%*									*
%************************************************************************
184

185
\begin{code}
186 187 188 189 190 191 192 193 194 195 196
tcInstType :: ([TyVar] -> TcM [TcTyVar]) 		-- How to instantiate the type variables
	   -> TcType 					-- Type to instantiate
	   -> TcM ([TcTyVar], TcThetaType, TcType)	-- Result
		-- (type vars (excl coercion vars), preds (incl equalities), rho)
tcInstType inst_tyvars ty
  = case tcSplitForAllTys ty of
	([],     rho) -> let	-- There may be overloading despite no type variables;
				-- 	(?x :: Int) => Int -> Int
			   (theta, tau) = tcSplitPhiTy rho
			 in
			 return ([], theta, tau)
197

198
	(tyvars, rho) -> do { tyvars' <- inst_tyvars tyvars
199

200 201
			    ; let  tenv = zipTopTvSubst tyvars (mkTyVarTys tyvars')
				-- Either the tyvars are freshly made, by inst_tyvars,
202 203
                                -- or any nested foralls have different binders.
                                -- Either way, zipTopTvSubst is ok
204

205 206
			    ; let  (theta, tau) = tcSplitPhiTy (substTy tenv rho)
			    ; return (tyvars', theta, tau) }
207

208
tcSkolDFunType :: Type -> TcM ([TcTyVar], TcThetaType, TcType)
209 210
-- Instantiate a type signature with skolem constants, but 
-- do *not* give them fresh names, because we want the name to
211
-- be in the type environment: it is lexically scoped.
212
tcSkolDFunType ty = tcInstType (\tvs -> return (tcSuperSkolTyVars tvs)) ty
213

214
tcSuperSkolTyVars :: [TyVar] -> [TcTyVar]
215
-- Make skolem constants, but do *not* give them new names, as above
216
-- Moreover, make them "super skolems"; see comments with superSkolemTv
dreixel's avatar
dreixel committed
217
-- see Note [Kind substitution when instantiating]
218 219 220 221 222 223
-- Precondition: tyvars should be ordered (kind vars first)
tcSuperSkolTyVars = snd . mapAccumL tcSuperSkolTyVar (mkTopTvSubst [])

tcSuperSkolTyVar :: TvSubst -> TyVar -> (TvSubst, TcTyVar)
tcSuperSkolTyVar subst tv
  = (extendTvSubst subst tv (mkTyVarTy new_tv), new_tv)
dreixel's avatar
dreixel committed
224
  where
225 226 227 228
    kind   = substTy subst (tyVarKind tv)
    new_tv = mkTcTyVar (tyVarName tv) kind superSkolemTv

tcInstSkolTyVar :: Bool -> TvSubst -> TyVar -> TcM (TvSubst, TcTyVar)
229
-- Instantiate the tyvar, using 
230 231 232
--      * the occ-name and kind of the supplied tyvar, 
--      * the unique from the monad,
--      * the location either from the tyvar (skol_info = SigSkol)
233
--                     or from the monad (otherwise)
dreixel's avatar
dreixel committed
234
tcInstSkolTyVar overlappable subst tyvar
235 236 237 238 239
  = do  { uniq <- newUnique
        ; loc  <- getSrcSpanM
        ; let new_name = mkInternalName uniq occ loc
              new_tv   = mkTcTyVar new_name kind (SkolemTv overlappable)
        ; return (extendTvSubst subst tyvar (mkTyVarTy new_tv), new_tv) }
240 241 242
  where
    old_name = tyVarName tyvar
    occ      = nameOccName old_name
dreixel's avatar
dreixel committed
243
    kind     = substTy subst (tyVarKind tyvar)
244

245
tcInstSkolTyVars' :: Bool -> TvSubst -> [TyVar] -> TcM (TvSubst, [TcTyVar])
dreixel's avatar
dreixel committed
246 247
-- Precondition: tyvars should be ordered (kind vars first)
-- see Note [Kind substitution when instantiating]
248
tcInstSkolTyVars' isSuperSkol = mapAccumLM (tcInstSkolTyVar isSuperSkol)
249

250 251 252 253
-- Wrappers
tcInstSkolTyVars, tcInstSuperSkolTyVars :: [TyVar] -> TcM [TcTyVar]
tcInstSkolTyVars      = fmap snd . tcInstSkolTyVars' False (mkTopTvSubst [])
tcInstSuperSkolTyVars = fmap snd . tcInstSkolTyVars' True  (mkTopTvSubst [])
dreixel's avatar
dreixel committed
254

255 256 257 258
tcInstSkolTyVarsX, tcInstSuperSkolTyVarsX
  :: TvSubst -> [TyVar] -> TcM (TvSubst, [TcTyVar])
tcInstSkolTyVarsX      subst = tcInstSkolTyVars' False subst
tcInstSuperSkolTyVarsX subst = tcInstSkolTyVars' True  subst
259 260

tcInstSkolType :: TcType -> TcM ([TcTyVar], TcThetaType, TcType)
261 262
-- Instantiate a type with fresh skolem constants
-- Binding location comes from the monad
263
tcInstSkolType ty = tcInstType tcInstSkolTyVars ty
264 265 266 267

tcInstSigTyVars :: [TyVar] -> TcM [TcTyVar]
-- Make meta SigTv type variables for patten-bound scoped type varaibles
-- We use SigTvs for them, so that they can't unify with arbitrary types
dreixel's avatar
dreixel committed
268 269
-- Precondition: tyvars should be ordered (kind vars first)
-- see Note [Kind substitution when instantiating]
270 271 272 273
tcInstSigTyVars = fmap snd . mapAccumLM tcInstSigTyVar (mkTopTvSubst [])

tcInstSigTyVar :: TvSubst -> TyVar -> TcM (TvSubst, TcTyVar)
tcInstSigTyVar subst tv
dreixel's avatar
dreixel committed
274 275
  = do { uniq <- newMetaUnique
       ; ref <- newMutVar Flexi
276 277 278 279 280 281
       ; let name   = setNameUnique (tyVarName tv) uniq
                      -- Use the same OccName so that the tidy-er
                      -- doesn't rename 'a' to 'a0' etc
             kind   = substTy subst (tyVarKind tv)
             new_tv = mkTcTyVar name kind (MetaTv SigTv ref)
       ; return (extendTvSubst subst tv (mkTyVarTy new_tv), new_tv) }
282 283
\end{code}

dreixel's avatar
dreixel committed
284 285 286 287 288 289 290 291 292 293 294 295 296 297 298
Note [Kind substitution when instantiating]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When we instantiate a bunch of kind and type variables, first we
expect them to be sorted (kind variables first, then type variables).
Then we have to instantiate the kind variables, build a substitution
from old variables to the new variables, then instantiate the type
variables substituting the original kind.

Exemple: If we want to instantiate
  [(k1 :: BOX), (k2 :: BOX), (a :: k1 -> k2), (b :: k1)]
we want
  [(?k1 :: BOX), (?k2 :: BOX), (?a :: ?k1 -> ?k2), (?b :: ?k1)]
instead of the buggous
  [(?k1 :: BOX), (?k2 :: BOX), (?a :: k1 -> k2), (?b :: k1)]

299 300 301

%************************************************************************
%*									*
302
	MetaTvs (meta type variables; mutable)
303 304 305 306
%*									*
%************************************************************************

\begin{code}
307
newMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar
308
-- Make a new meta tyvar out of thin air
309
newMetaTyVar meta_info kind
310
  = do	{ uniq <- newMetaUnique
311
 	; ref <- newMutVar Flexi
312 313
        ; let name = mkTcTyVarName uniq s
              s = case meta_info of
Simon Peyton Jones's avatar
Simon Peyton Jones committed
314 315 316
                        TauTv -> fsLit "t"
                        TcsTv -> fsLit "u"
                        SigTv -> fsLit "a"
317
	; return (mkTcTyVar name kind (MetaTv meta_info ref)) }
318

319 320 321 322 323
mkTcTyVarName :: Unique -> FastString -> Name
-- Make sure that fresh TcTyVar names finish with a digit
-- leaving the un-cluttered names free for user names
mkTcTyVarName uniq str = mkSysTvName uniq str

dreixel's avatar
dreixel committed
324
-- Works for both type and kind variables
325 326 327 328
readMetaTyVar :: TyVar -> TcM MetaDetails
readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
		      readMutVar (metaTvRef tyvar)

329 330 331 332 333 334 335 336 337
isFilledMetaTyVar :: TyVar -> TcM Bool
-- True of a filled-in (Indirect) meta type variable
isFilledMetaTyVar tv
  | not (isTcTyVar tv) = return False
  | MetaTv _ ref <- tcTyVarDetails tv
  = do 	{ details <- readMutVar ref
	; return (isIndirect details) }
  | otherwise = return False

338 339 340 341 342 343 344 345 346 347
isFlexiMetaTyVar :: TyVar -> TcM Bool
-- True of a un-filled-in (Flexi) meta type variable
isFlexiMetaTyVar tv
  | not (isTcTyVar tv) = return False
  | MetaTv _ ref <- tcTyVarDetails tv
  = do 	{ details <- readMutVar ref
	; return (isFlexi details) }
  | otherwise = return False

--------------------
dreixel's avatar
dreixel committed
348
-- Works with both type and kind variables
349
writeMetaTyVar :: TcTyVar -> TcType -> TcM ()
350 351
-- Write into a currently-empty MetaTyVar

Ian Lynagh's avatar
Ian Lynagh committed
352
writeMetaTyVar tyvar ty
353 354 355 356 357 358 359 360 361 362 363 364 365
  | not debugIsOn 
  = writeMetaTyVarRef tyvar (metaTvRef tyvar) ty

-- Everything from here on only happens if DEBUG is on
  | not (isTcTyVar tyvar)
  = WARN( True, text "Writing to non-tc tyvar" <+> ppr tyvar )
    return ()

  | MetaTv _ ref <- tcTyVarDetails tyvar
  = writeMetaTyVarRef tyvar ref ty

  | otherwise
  = WARN( True, text "Writing to non-meta tyvar" <+> ppr tyvar )
366
    return ()
367 368 369 370 371 372 373 374 375 376 377

--------------------
writeMetaTyVarRef :: TcTyVar -> TcRef MetaDetails -> TcType -> TcM ()
-- Here the tyvar is for error checking only; 
-- the ref cell must be for the same tyvar
writeMetaTyVarRef tyvar ref ty
  | not debugIsOn 
  = do { traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
       ; writeMutVar ref (Indirect ty) }

-- Everything from here on only happens if DEBUG is on
378
  | otherwise
379
  = do { meta_details <- readMutVar ref; 
dreixel's avatar
dreixel committed
380 381 382 383 384
       -- Zonk kinds to allow the error check to work
       ; zonked_tv_kind <- zonkTcKind tv_kind 
       ; zonked_ty_kind <- zonkTcKind ty_kind

       -- Check for double updates
385 386
       ; ASSERT2( isFlexi meta_details, 
                  hang (text "Double update of meta tyvar")
387 388 389
                   2 (ppr tyvar $$ ppr meta_details) )

         traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
dreixel's avatar
dreixel committed
390 391 392 393 394 395 396 397 398
       ; writeMutVar ref (Indirect ty) 
       ; when (   not (isPredTy tv_kind) 
                    -- Don't check kinds for updates to coercion variables
               && not (zonked_ty_kind `isSubKind` zonked_tv_kind))
       $ WARN( True, hang (text "Ill-kinded update to meta tyvar")
                        2 (    ppr tyvar <+> text "::" <+> ppr tv_kind 
                           <+> text ":=" 
                           <+> ppr ty    <+> text "::" <+> ppr ty_kind) )
         (return ()) }
399 400 401
  where
    tv_kind = tyVarKind tyvar
    ty_kind = typeKind ty
402 403
\end{code}

404 405 406 407 408 409 410 411 412 413 414 415

%************************************************************************
%*									*
	MetaTvs: TauTvs
%*									*
%************************************************************************

\begin{code}
newFlexiTyVar :: Kind -> TcM TcTyVar
newFlexiTyVar kind = newMetaTyVar TauTv kind

newFlexiTyVarTy  :: Kind -> TcM TcType
416 417 418
newFlexiTyVarTy kind = do
    tc_tyvar <- newFlexiTyVar kind
    return (TyVarTy tc_tyvar)
419 420

newFlexiTyVarTys :: Int -> Kind -> TcM [TcType]
421
newFlexiTyVarTys n kind = mapM newFlexiTyVarTy (nOfThem n kind)
422 423 424

tcInstTyVars :: [TyVar] -> TcM ([TcTyVar], [TcType], TvSubst)
-- Instantiate with META type variables
dreixel's avatar
dreixel committed
425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444
tcInstTyVars tyvars = tcInstTyVarsX emptyTvSubst tyvars
    -- emptyTvSubst has an empty in-scope set, but that's fine here
    -- Since the tyvars are freshly made, they cannot possibly be
    -- captured by any existing for-alls.

tcInstTyVarsX :: TvSubst -> [TyVar] -> TcM ([TcTyVar], [TcType], TvSubst)
tcInstTyVarsX subst tyvars =
  do { (subst', tyvars') <- mapAccumLM tcInstTyVar subst tyvars
     ; return (tyvars', mkTyVarTys tyvars', subst') }

tcInstTyVar :: TvSubst -> TyVar -> TcM (TvSubst, TcTyVar)
-- Make a new unification variable tyvar whose Name and Kind come from
-- an existing TyVar. We substitute kind variables in the kind.
tcInstTyVar subst tyvar
  = do  { uniq <- newMetaUnique
        ; ref <- newMutVar Flexi
        ; let name   = mkSystemName uniq (getOccName tyvar)
              kind   = substTy subst (tyVarKind tyvar)
              new_tv = mkTcTyVar name kind (MetaTv TauTv ref)
        ; return (extendTvSubst subst tyvar (mkTyVarTy new_tv), new_tv) }
445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470
\end{code}


%************************************************************************
%*									*
	MetaTvs: SigTvs
%*									*
%************************************************************************

\begin{code}
zonkSigTyVar :: TcTyVar -> TcM TcTyVar
zonkSigTyVar sig_tv 
  | isSkolemTyVar sig_tv 
  = return sig_tv	-- Happens in the call in TcBinds.checkDistinctTyVars
  | otherwise
  = ASSERT( isSigTyVar sig_tv )
    do { ty <- zonkTcTyVar sig_tv
       ; return (tcGetTyVar "zonkSigTyVar" ty) }
	-- 'ty' is bound to be a type variable, because SigTvs
	-- can only be unified with type variables
\end{code}



%************************************************************************
%*									*
471
\subsection{Zonking -- the exernal interfaces}
472 473 474
%*									*
%************************************************************************

475 476 477
@tcGetGlobalTyVars@ returns a fully-zonked set of tyvars free in the environment.
To improve subsequent calls to the same function it writes the zonked set back into
the environment.
478 479

\begin{code}
480 481 482 483
tcGetGlobalTyVars :: TcM TcTyVarSet
tcGetGlobalTyVars
  = do { (TcLclEnv {tcl_tyvars = gtv_var}) <- getLclEnv
       ; gbl_tvs  <- readMutVar gtv_var
484
       ; gbl_tvs' <- zonkTcTyVarsAndFV gbl_tvs
485 486
       ; writeMutVar gtv_var gbl_tvs'
       ; return gbl_tvs' }
487 488 489 490 491
\end{code}

-----------------  Type variables

\begin{code}
492
zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
493
zonkTcTyVars tyvars = mapM zonkTcTyVar tyvars
494

495 496
zonkTcTyVarsAndFV :: TcTyVarSet -> TcM TcTyVarSet
zonkTcTyVarsAndFV tyvars = tyVarsOfTypes <$> mapM zonkTcTyVar (varSetElems tyvars)
497 498

-----------------  Types
499
zonkTcTypeCarefully :: TcType -> TcM TcType
500
-- Do not zonk type variables free in the environment
501 502 503
zonkTcTypeCarefully ty = zonkTcType ty   -- I think this function is out of date

{-
504
  = do { env_tvs <- tcGetGlobalTyVars
505 506 507 508 509 510 511 512
       ; zonkType (zonk_tv env_tvs) ty }
  where
    zonk_tv env_tvs tv
      | tv `elemVarSet` env_tvs 
      = return (TyVarTy tv)
      | otherwise
      = ASSERT( isTcTyVar tv )
    	case tcTyVarDetails tv of
513 514 515 516 517
          SkolemTv {}   -> return (TyVarTy tv)
          RuntimeUnk {} -> return (TyVarTy tv)
          FlatSkol ty   -> zonkType (zonk_tv env_tvs) ty
          MetaTv _ ref  -> do { cts <- readMutVar ref
                              ; case cts of
518 519
			           Flexi       -> return (TyVarTy tv)
			           Indirect ty -> zonkType (zonk_tv env_tvs) ty }
520
-}
521

522
zonkTcType :: TcType -> TcM TcType
523 524 525 526 527 528
-- Simply look through all Flexis
zonkTcType ty = zonkType zonkTcTyVar ty

zonkTcTyVar :: TcTyVar -> TcM TcType
-- Simply look through all Flexis
zonkTcTyVar tv
dreixel's avatar
dreixel committed
529
  = ASSERT2( isTcTyVar tv, ppr tv ) do
530
    case tcTyVarDetails tv of
dreixel's avatar
dreixel committed
531 532
      SkolemTv {}   -> zonk_kind_and_return
      RuntimeUnk {} -> zonk_kind_and_return
533 534 535
      FlatSkol ty   -> zonkTcType ty
      MetaTv _ ref  -> do { cts <- readMutVar ref
                          ; case cts of
dreixel's avatar
dreixel committed
536
		               Flexi       -> zonk_kind_and_return
537
			       Indirect ty -> zonkTcType ty }
dreixel's avatar
dreixel committed
538 539 540 541 542 543 544
  where
    zonk_kind_and_return = do { z_tv <- zonkTyVarKind tv
                              ; return (TyVarTy z_tv) }

zonkTyVarKind :: TyVar -> TcM TyVar
zonkTyVarKind tv = do { kind' <- zonkTcKind (tyVarKind tv)
                      ; return (setTyVarKind tv kind') }
545

546 547 548 549
zonkTcTypeAndSubst :: TvSubst -> TcType -> TcM TcType
-- Zonk, and simultaneously apply a non-necessarily-idempotent substitution
zonkTcTypeAndSubst subst ty = zonkType zonk_tv ty
  where
dreixel's avatar
dreixel committed
550 551 552 553 554 555 556 557 558 559
    zonk_tv tv
      = do { z_tv <- updateTyVarKindM zonkTcKind tv
           ; case tcTyVarDetails tv of
                SkolemTv {}   -> return (TyVarTy z_tv)
                RuntimeUnk {} -> return (TyVarTy z_tv)
                FlatSkol ty   -> zonkType zonk_tv ty
                MetaTv _ ref  -> do { cts <- readMutVar ref
                                    ; case cts of
      			           Flexi       -> zonk_flexi z_tv
      			           Indirect ty -> zonkType zonk_tv ty } }
560 561 562 563 564
    zonk_flexi tv
      = case lookupTyVar subst tv of
          Just ty -> zonkType zonk_tv ty
          Nothing -> return (TyVarTy tv)

565
zonkTcTypes :: [TcType] -> TcM [TcType]
566
zonkTcTypes tys = mapM zonkTcType tys
567

568
zonkTcThetaType :: TcThetaType -> TcM TcThetaType
569
zonkTcThetaType theta = mapM zonkTcPredType theta
570

571
zonkTcPredType :: TcPredType -> TcM TcPredType
batterseapower's avatar
batterseapower committed
572
zonkTcPredType = zonkTcType
573 574 575 576 577 578
\end{code}

-------------------  These ...ToType, ...ToKind versions
		     are used at the end of type checking

\begin{code}
dreixel's avatar
dreixel committed
579
defaultKindVarToStar :: TcTyVar -> TcM Kind
dreixel's avatar
dreixel committed
580 581
-- We have a meta-kind: unify it with '*'
defaultKindVarToStar kv 
dreixel's avatar
dreixel committed
582 583 584
  = do { ASSERT ( isKiVar kv && isMetaTyVar kv )
         writeMetaTyVar kv liftedTypeKind
       ; return liftedTypeKind }
dreixel's avatar
dreixel committed
585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605

zonkQuantifiedTyVars :: TcTyVarSet -> TcM [TcTyVar]
-- Precondition: a kind variable occurs before a type
--               variable mentioning it in its kind
zonkQuantifiedTyVars tyvars
  = do { let (kvs, tvs) = partitionKiTyVars (varSetElems tyvars)
       ; poly_kinds <- xoptM Opt_PolyKinds
       ; if poly_kinds then
             mapM zonkQuantifiedTyVar (kvs ++ tvs)
           -- Because of the order, any kind variables
           -- mentioned in the kinds of the type variables refer to
           -- the now-quantified versions
         else
             -- In the non-PolyKinds case, default the kind variables
             -- to *, and zonk the tyvars as usual.  Notice that this
             -- may make zonkQuantifiedTyVars return a shorter list
             -- than it was passed, but that's ok
             do { let (meta_kvs, skolem_kvs) = partition isMetaTyVar kvs
                ; WARN ( not (null skolem_kvs), ppr skolem_kvs )
                  mapM_ defaultKindVarToStar meta_kvs
                ; mapM zonkQuantifiedTyVar (skolem_kvs ++ tvs) } }
606

607
zonkQuantifiedTyVar :: TcTyVar -> TcM TcTyVar
608 609 610 611
-- The quantified type variables often include meta type variables
-- we want to freeze them into ordinary type variables, and
-- default their kind (e.g. from OpenTypeKind to TypeKind)
-- 			-- see notes with Kind.defaultKind
612
-- The meta tyvar is updated to point to the new skolem TyVar.  Now any 
613 614 615
-- bound occurences of the original type variable will get zonked to 
-- the immutable version.
--
616
-- We leave skolem TyVars alone; they are immutable.
dreixel's avatar
dreixel committed
617 618 619
--
-- This function is called on both kind and type variables,
-- but kind variables *only* if PolyKinds is on.
620
zonkQuantifiedTyVar tv
621 622
  = ASSERT2( isTcTyVar tv, ppr tv ) 
    case tcTyVarDetails tv of
dreixel's avatar
dreixel committed
623
      SkolemTv {} -> do { kind <- zonkTcKind (tyVarKind tv)
624
                        ; return $ setTyVarKind tv kind }
625 626 627
	-- It might be a skolem type variable, 
	-- for example from a user type signature

Ian Lynagh's avatar
Ian Lynagh committed
628 629 630 631 632 633 634 635 636 637
      MetaTv _ ref ->
          do when debugIsOn $ do
                 -- [Sept 04] Check for non-empty.
                 -- See note [Silly Type Synonym]
                 cts <- readMutVar ref
                 case cts of
                     Flexi -> return ()
                     Indirect ty -> WARN( True, ppr tv $$ ppr ty )
                                    return ()
             skolemiseUnboundMetaTyVar tv vanillaSkolemTv
638 639 640
      _other -> pprPanic "zonkQuantifiedTyVar" (ppr tv) -- FlatSkol, RuntimeUnk

skolemiseUnboundMetaTyVar :: TcTyVar -> TcTyVarDetails -> TcM TyVar
641 642 643 644 645
-- We have a Meta tyvar with a ref-cell inside it
-- Skolemise it, including giving it a new Name, so that
--   we are totally out of Meta-tyvar-land
-- We create a skolem TyVar, not a regular TyVar
--   See Note [Zonking to Skolem]
646
skolemiseUnboundMetaTyVar tv details
647
  = ASSERT2( isMetaTyVar tv, ppr tv ) 
648 649 650
    do  { span <- getSrcSpanM    -- Get the location from "here"
                                 -- ie where we are generalising
        ; uniq <- newUnique      -- Remove it from TcMetaTyVar unique land
dreixel's avatar
dreixel committed
651 652
        ; kind <- zonkTcKind (tyVarKind tv)
        ; let final_kind = defaultKind kind
653 654
              final_name = mkInternalName uniq (getOccName tv) span
              final_tv   = mkTcTyVar final_name final_kind details
dreixel's avatar
dreixel committed
655 656 657

        ; writeMetaTyVar tv (mkTyVarTy final_tv)
        ; return final_tv }
658 659
\end{code}

660 661
\begin{code}
zonkImplication :: Implication -> TcM Implication
662
zonkImplication implic@(Implic { ic_given = given 
663 664 665 666 667 668 669 670 671
                               , ic_wanted = wanted
                               , ic_loc = loc })
  = do {    -- No need to zonk the skolems
       ; given'  <- mapM zonkEvVar given
       ; loc'    <- zonkGivenLoc loc
       ; wanted' <- zonkWC wanted
       ; return (implic { ic_given = given'
                        , ic_wanted = wanted'
                        , ic_loc = loc' }) }
672 673 674 675 676

zonkEvVar :: EvVar -> TcM EvVar
zonkEvVar var = do { ty' <- zonkTcType (varType var)
                   ; return (setVarType var ty') }

677 678 679

zonkWC :: WantedConstraints -> TcM WantedConstraints
zonkWC (WC { wc_flat = flat, wc_impl = implic, wc_insol = insol })
680
  = do { flat'   <- mapBagM zonkCt flat 
681
       ; implic' <- mapBagM zonkImplication implic
682
       ; insol'  <- mapBagM zonkCt insol
683 684
       ; return (WC { wc_flat = flat', wc_impl = implic', wc_insol = insol' }) }

685 686 687 688 689 690 691 692 693 694 695 696
zonkCt :: Ct -> TcM Ct 
-- Zonking a Ct conservatively gives back a CNonCanonical
zonkCt ct 
  = do { v'  <- zonkEvVar (cc_id ct)
       ; fl' <- zonkFlavor (cc_flavor ct)
       ; return $ 
         CNonCanonical { cc_id = v'
                       , cc_flavor = fl'
                       , cc_depth = cc_depth ct } }
zonkCts :: Cts -> TcM Cts
zonkCts = mapBagM zonkCt

697 698
zonkWantedEvVars :: Bag WantedEvVar -> TcM (Bag WantedEvVar)
zonkWantedEvVars = mapBagM zonkWantedEvVar
699 700

zonkWantedEvVar :: WantedEvVar -> TcM WantedEvVar
701 702 703
zonkWantedEvVar (EvVarX v l) = do { v' <- zonkEvVar v; return (EvVarX v' l) }

zonkFlavor :: CtFlavor -> TcM CtFlavor
dimitris's avatar
dimitris committed
704 705
zonkFlavor (Given loc gk) = do { loc' <- zonkGivenLoc loc; return (Given loc' gk) }
zonkFlavor fl             = return fl
706 707 708 709 710 711 712 713 714 715 716 717 718 719 720

zonkGivenLoc :: GivenLoc -> TcM GivenLoc
-- GivenLocs may have unification variables inside them!
zonkGivenLoc (CtLoc skol_info span ctxt)
  = do { skol_info' <- zonkSkolemInfo skol_info
       ; return (CtLoc skol_info' span ctxt) }

zonkSkolemInfo :: SkolemInfo -> TcM SkolemInfo
zonkSkolemInfo (SigSkol cx ty)  = do { ty' <- zonkTcType ty
                                     ; return (SigSkol cx ty') }
zonkSkolemInfo (InferSkol ntys) = do { ntys' <- mapM do_one ntys
                                     ; return (InferSkol ntys') }
  where
    do_one (n, ty) = do { ty' <- zonkTcType ty; return (n, ty') }
zonkSkolemInfo skol_info = return skol_info
721 722
\end{code}

723 724
Note [Silly Type Synonyms]
~~~~~~~~~~~~~~~~~~~~~~~~~~
725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741
Consider this:
	type C u a = u	-- Note 'a' unused

	foo :: (forall a. C u a -> C u a) -> u
	foo x = ...

	bar :: Num u => u
	bar = foo (\t -> t + t)

* From the (\t -> t+t) we get type  {Num d} =>  d -> d
  where d is fresh.

* Now unify with type of foo's arg, and we get:
	{Num (C d a)} =>  C d a -> C d a
  where a is fresh.

* Now abstract over the 'a', but float out the Num (C d a) constraint
742
  because it does not 'really' mention a.  (see exactTyVarsOfType)
743
  The arg to foo becomes
Ian Lynagh's avatar
Ian Lynagh committed
744
	\/\a -> \t -> t+t
745 746 747

* So we get a dict binding for Num (C d a), which is zonked to give
	a = ()
748 749 750 751
  [Note Sept 04: now that we are zonking quantified type variables
  on construction, the 'a' will be frozen as a regular tyvar on
  quantification, so the floated dict will still have type (C d a).
  Which renders this whole note moot; happily!]
752

Ian Lynagh's avatar
Ian Lynagh committed
753
* Then the \/\a abstraction has a zonked 'a' in it.
754

755
All very silly.   I think its harmless to ignore the problem.  We'll end up with
Ian Lynagh's avatar
Ian Lynagh committed
756
a \/\a in the final result but all the occurrences of a will be zonked to ()
757

758 759 760 761 762 763 764 765 766 767 768
Note [Zonking to Skolem]
~~~~~~~~~~~~~~~~~~~~~~~~
We used to zonk quantified type variables to regular TyVars.  However, this
leads to problems.  Consider this program from the regression test suite:

  eval :: Int -> String -> String -> String
  eval 0 root actual = evalRHS 0 root actual

  evalRHS :: Int -> a
  evalRHS 0 root actual = eval 0 root actual

769
It leads to the deferral of an equality (wrapped in an implication constraint)
770

dreixel's avatar
dreixel committed
771
  forall a. () => ((String -> String -> String) ~ a)
772 773 774 775 776 777 778 779 780 781 782 783 784 785

which is propagated up to the toplevel (see TcSimplify.tcSimplifyInferCheck).
In the meantime `a' is zonked and quantified to form `evalRHS's signature.
This has the *side effect* of also zonking the `a' in the deferred equality
(which at this point is being handed around wrapped in an implication
constraint).

Finally, the equality (with the zonked `a') will be handed back to the
simplifier by TcRnDriver.tcRnSrcDecls calling TcSimplify.tcSimplifyTop.
If we zonk `a' with a regular type variable, we will have this regular type
variable now floating around in the simplifier, which in many places assumes to
only see proper TcTyVars.

We can avoid this problem by zonking with a skolem.  The skolem is rigid
786
(which we require for a quantified variable), but is still a TcTyVar that the
787 788
simplifier knows how to deal with.

789 790 791 792 793 794 795 796 797 798 799 800 801 802

%************************************************************************
%*									*
\subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
%*									*
%*		For internal use only!					*
%*									*
%************************************************************************

\begin{code}
-- For unbound, mutable tyvars, zonkType uses the function given to it
-- For tyvars bound at a for-all, zonkType zonks them to an immutable
--	type variable and zonks the kind too

dreixel's avatar
dreixel committed
803 804 805
zonkKind :: (TcTyVar -> TcM Kind) -> TcKind -> TcM Kind
zonkKind = zonkType

806 807
zonkType :: (TcTyVar -> TcM Type)  -- What to do with TcTyVars
         -> TcType -> TcM Type
808
zonkType zonk_tc_tyvar ty
809 810
  = go ty
  where
811 812 813 814 815 816 817 818 819 820
    go (TyConApp tc tys) = do tys' <- mapM go tys
                              return (TyConApp tc tys')

    go (FunTy arg res)   = do arg' <- go arg
                              res' <- go res
                              return (FunTy arg' res')

    go (AppTy fun arg)   = do fun' <- go fun
                              arg' <- go arg
                              return (mkAppTy fun' arg')
821 822 823
		-- NB the mkAppTy; we might have instantiated a
		-- type variable to a type constructor, so we need
		-- to pull the TyConApp to the top.
824 825

	-- The two interesting cases!
826
    go (TyVarTy tyvar) | isTcTyVar tyvar = zonk_tc_tyvar tyvar
dreixel's avatar
dreixel committed
827
		       | otherwise	 = TyVarTy <$> updateTyVarKindM zonkTcKind tyvar
828
		-- Ordinary (non Tc) tyvars occur inside quantified types
829

830 831
    go (ForAllTy tyvar ty) = ASSERT( isImmutableTyVar tyvar ) do
                             ty' <- go ty
dreixel's avatar
dreixel committed
832
                             tyvar' <- updateTyVarKindM zonkTcKind tyvar
833
                             return (ForAllTy tyvar' ty')
834 835 836 837
\end{code}



838 839 840 841 842 843 844
%************************************************************************
%*									*
			Zonking kinds
%*									*
%************************************************************************

\begin{code}
dreixel's avatar
dreixel committed
845 846 847 848 849 850 851 852 853 854 855
compatKindTcM :: Kind -> Kind -> TcM Bool
compatKindTcM k1 k2
  = do { k1' <- zonkTcKind k1
       ; k2' <- zonkTcKind k2
       ; return $ k1' `isSubKind` k2' || k2' `isSubKind` k1' }

isSubKindTcM :: Kind -> Kind -> TcM Bool
isSubKindTcM k1 k2
  = do { k1' <- zonkTcKind k1
       ; k2' <- zonkTcKind k2
       ; return $ k1' `isSubKind` k2' }
856 857 858

-------------
zonkTcKind :: TcKind -> TcM TcKind
859
zonkTcKind k = zonkTcType k
860 861
\end{code}
			
862 863
%************************************************************************
%*									*
864 865 866 867 868 869 870 871 872
\subsection{Checking a user type}
%*									*
%************************************************************************

When dealing with a user-written type, we first translate it from an HsType
to a Type, performing kind checking, and then check various things that should 
be true about it.  We don't want to perform these checks at the same time
as the initial translation because (a) they are unnecessary for interface-file
types and (b) when checking a mutually recursive group of type and class decls,
873 874
we can't "look" at the tycons/classes yet.  Also, the checks are are rather
diverse, and used to really mess up the other code.
875 876 877 878 879 880 881 882 883 884 885 886 887 888

One thing we check for is 'rank'.  

	Rank 0: 	monotypes (no foralls)
	Rank 1:		foralls at the front only, Rank 0 inside
	Rank 2:		foralls at the front, Rank 1 on left of fn arrow,

	basic ::= tyvar | T basic ... basic

	r2  ::= forall tvs. cxt => r2a
	r2a ::= r1 -> r2a | basic
	r1  ::= forall tvs. cxt => r0
	r0  ::= r0 -> r0 | basic
	
889 890 891 892 893
Another thing is to check that type synonyms are saturated. 
This might not necessarily show up in kind checking.
	type A i = i
	data T k = MkT (k Int)
	f :: T A	-- BAD!
894

895
	
896
\begin{code}
897 898 899 900 901 902 903 904 905 906 907
-- Depending on the context, we might accept any kind (for instance, in a TH
-- splice), or only certain kinds (like in type signatures).
expectedKindInCtxt :: UserTypeCtxt -> Maybe Kind
expectedKindInCtxt (TySynCtxt _)  = Nothing -- Any kind will do
expectedKindInCtxt ThBrackCtxt    = Nothing
expectedKindInCtxt GhciCtxt       = Nothing
expectedKindInCtxt ResSigCtxt     = Just openTypeKind
expectedKindInCtxt ExprSigCtxt    = Just openTypeKind
expectedKindInCtxt (ForSigCtxt _) = Just liftedTypeKind
expectedKindInCtxt _              = Just argTypeKind

908 909
checkValidType :: UserTypeCtxt -> Type -> TcM ()
-- Checks that the type is valid for the given context
910
checkValidType ctxt ty = do
dreixel's avatar
dreixel committed
911 912 913 914 915 916
    traceTc "checkValidType" (ppr ty <+> text "::" <+> ppr (typeKind ty))
    unboxed         <- xoptM Opt_UnboxedTuples
    rank2           <- xoptM Opt_Rank2Types
    rankn           <- xoptM Opt_RankNTypes
    polycomp        <- xoptM Opt_PolymorphicComponents
    constraintKinds <- xoptM Opt_ConstraintKinds
917
    let 
918 919 920 921 922 923 924 925 926 927
	gen_rank n | rankn     = ArbitraryRank
	           | rank2     = Rank 2
	           | otherwise = Rank n
	rank
	  = case ctxt of
		 DefaultDeclCtxt-> MustBeMonoType
		 ResSigCtxt	-> MustBeMonoType
		 LamPatSigCtxt	-> gen_rank 0
		 BindPatSigCtxt	-> gen_rank 0
		 TySynCtxt _    -> gen_rank 0
928

929 930
		 ExprSigCtxt 	-> gen_rank 1
		 FunSigCtxt _   -> gen_rank 1
931
		 InfSigCtxt _   -> ArbitraryRank	-- Inferred type
932
		 ConArgCtxt _   | polycomp -> gen_rank 2
Ian Lynagh's avatar
Ian Lynagh committed
933 934
                                -- We are given the type of the entire
                                -- constructor, hence rank 1
935
 				| otherwise -> gen_rank 1
936

937 938
		 ForSigCtxt _	-> gen_rank 1
		 SpecInstCtxt   -> gen_rank 1
939
                 ThBrackCtxt    -> gen_rank 1
940
		 GhciCtxt       -> ArbitraryRank
dreixel's avatar
dreixel committed
941 942
                 _              -> panic "checkValidType"
                                     -- Can't happen; not used for *user* sigs
943 944 945

	actual_kind = typeKind ty

946 947 948
        kind_ok = case expectedKindInCtxt ctxt of
                    Nothing -> True
                    Just k  -> tcIsSubKind actual_kind k
949
	
950 951 952 953 954 955 956 957
	ubx_tup 
         | not unboxed = UT_NotOk
         | otherwise   = case ctxt of
	              	   TySynCtxt _ -> UT_Ok
	              	   ExprSigCtxt -> UT_Ok
	              	   ThBrackCtxt -> UT_Ok
		      	   GhciCtxt    -> UT_Ok
	              	   _           -> UT_NotOk
958

959
	-- Check the internal validity of the type itself
960
    check_type rank ubx_tup ty
961

962
	-- Check that the thing has kind Type, and is lifted if necessary
dreixel's avatar
dreixel committed
963
	-- Do this second, because we can't usefully take the kind of an 
964 965 966
	-- ill-formed type such as (a~Int)
    checkTc kind_ok (kindErr actual_kind)

dreixel's avatar
dreixel committed
967 968 969 970
        -- Check that the thing does not have kind Constraint,
        -- if -XConstraintKinds isn't enabled
    unless constraintKinds
      $ checkTc (not (isConstraintKind actual_kind)) (predTupleErr ty)
971 972

checkValidMonoType :: Type -> TcM ()
973
checkValidMonoType ty = check_mono_type MustBeMonoType ty
974 975 976 977
\end{code}


\begin{code}
978 979 980
data Rank = ArbitraryRank	  -- Any rank ok
          | MustBeMonoType  	  -- Monotype regardless of flags
	  | TyConArgMonoType	  -- Monotype but could be poly if -XImpredicativeTypes
981
	  | SynArgMonoType	  -- Monotype but could be poly if -XLiberalTypeSynonyms
982
          | Rank Int		  -- Rank n, but could be more with -XRankNTypes
983

984 985 986 987
decRank :: Rank -> Rank		  -- Function arguments
decRank (Rank 0)   = Rank 0
decRank (Rank n)   = Rank (n-1)
decRank other_rank = other_rank
988

989
nonZeroRank :: Rank -> Bool
990 991 992
nonZeroRank ArbitraryRank = True
nonZeroRank (Rank n) 	  = n>0
nonZeroRank _        	  = False
993

994 995
----------------------------------------
data UbxTupFlag = UT_Ok	| UT_NotOk
996
	-- The "Ok" version means "ok if UnboxedTuples is on"
997 998

----------------------------------------
dreixel's avatar
dreixel committed
999
check_mono_type :: Rank -> KindOrType -> TcM ()	-- No foralls anywhere
1000 1001
				      		-- No unlifted types of any kind
check_mono_type rank ty
dreixel's avatar
dreixel committed
1002 1003
  | isKind ty = return ()  -- IA0_NOTE: Do we need to check kinds?
  | otherwise
1004
   = do { check_type rank UT_NotOk ty
1005 1006 1007
	; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }

check_type :: Rank -> UbxTupFlag -> Type -> TcM ()
1008
-- The args say what the *type context* requires, independent
1009 1010 1011 1012 1013 1014 1015
-- of *flag* settings.  You test the flag settings at usage sites.
-- 
-- Rank is allowed rank for function args
-- Rank 0 means no for-alls anywhere

check_type rank ubx_tup ty
  | not (null tvs && null theta)
1016
  = do	{ checkTc (nonZeroRank rank) (forAllTyErr rank ty)
1017 1018 1019 1020
		-- Reject e.g. (Maybe (?x::Int => Int)), 
		-- with a decent error message
	; check_valid_theta SigmaCtxt theta
	; check_type rank ubx_tup tau	-- Allow foralls to right of arrow
1021 1022 1023 1024
	; checkAmbiguity tvs theta (tyVarsOfType tau) }
  where
    (tvs, theta, tau) = tcSplitSigmaTy ty
   
Ian Lynagh's avatar
Ian Lynagh committed
1025
check_type _ _ (TyVarTy _) = return ()
1026

Ian Lynagh's avatar
Ian Lynagh committed
1027
check_type rank _ (FunTy arg_ty res_ty)
1028 1029
  = do	{ check_type (decRank rank) UT_NotOk arg_ty
	; check_type rank 	    UT_Ok    res_ty }
1030

Ian Lynagh's avatar
Ian Lynagh committed
1031
check_type rank _ (AppTy ty1 ty2)
1032 1033
  = do	{ check_arg_type rank ty1
	; check_arg_type rank ty2 }
1034

1035
check_type rank ubx_tup ty@(TyConApp tc tys)
1036 1037
  | isSynTyCon tc
  = do	{ 	-- Check that the synonym has enough args
1038
		-- This applies equally to open and closed synonyms
1039
	 	-- It's OK to have an *over-applied* type synonym
1040 1041 1042
		--	data Tree a b = ...
		--	type Foo a = Tree [a]
		--	f :: Foo a b -> ...
1043 1044 1045
 	  checkTc (tyConArity tc <= length tys) arity_msg

	-- See N