TcMType.lhs 73 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]
27
  newMetaKindVar, newMetaKindVars, mkKindSigVar,
28
  mkTcTyVarName, cloneMetaTyVar, 
29

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

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

38
  newWantedEvVar, newWantedEvVars,
39
  newTcEvBinds, addTcEvBind,
40

41 42
  --------------------------------
  -- Instantiation
43
  tcInstTyVars, tcInstSigTyVars, newSigTyVar,
Simon Peyton Jones's avatar
Simon Peyton Jones committed
44
  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
  growThetaTyVars, quantifyPred,
59

60 61
  --------------------------------
  -- Zonking
62
  zonkTcPredType, 
63
  skolemiseSigTv, skolemiseUnboundMetaTyVar,
64
  zonkTcTyVar, zonkTcTyVars, zonkTyVarsAndFV, 
65
  zonkQuantifiedTyVar, zonkQuantifiedTyVars,
Ian Lynagh's avatar
Ian Lynagh committed
66
  zonkTcType, zonkTcTypes, zonkTcThetaType,
67

68
  zonkTcKind, defaultKindVarToStar,
69
  zonkEvVar, zonkWC, zonkId, zonkCt, zonkCts, zonkSkolemInfo,
70

71
  tcGetGlobalTyVars, 
72 73 74 75 76
  ) where

#include "HsVersions.h"

-- friends:
77 78
import TypeRep
import TcType
79
import TcEvidence
80
import Type
dreixel's avatar
dreixel committed
81
import Kind
82 83 84
import Class
import TyCon
import Var
85 86

-- others:
87 88
import HsSyn		-- HsType
import TcRnMonad        -- TcType, amongst others
89
import Id
90 91
import FunDeps
import Name
92
import VarSet
93
import ErrUtils
94
import PrelNames
95 96
import DynFlags
import Util
97
import Maybes
98
import ListSetOps
99
import SrcLoc
100
import Outputable
101
import FastString
102
import Bag
103

Ian Lynagh's avatar
Ian Lynagh committed
104
import Control.Monad
105
import Data.List        ( (\\), partition, mapAccumL )
106 107 108 109 110
\end{code}


%************************************************************************
%*									*
111
	Kind variables
112 113 114 115
%*									*
%************************************************************************

\begin{code}
116 117 118 119 120 121 122
mkKindName :: Unique -> Name
mkKindName unique = mkSystemName unique kind_var_occ

kind_var_occ :: OccName	-- Just one for all MetaKindVars
			-- They may be jiggled by tidying
kind_var_occ = mkOccName tvName "k"

dreixel's avatar
dreixel committed
123
newMetaKindVar :: TcM TcKind
124
newMetaKindVar = do { uniq <- newUnique
125 126 127
		    ; details <- newMetaDetails TauTv
                    ; let kv = mkTcTyVar (mkKindName uniq) superKind details
		    ; return (mkTyVarTy kv) }
128

dreixel's avatar
dreixel committed
129 130
newMetaKindVars :: Int -> TcM [TcKind]
newMetaKindVars n = mapM (\ _ -> newMetaKindVar) (nOfThem n ())
131 132 133 134

mkKindSigVar :: Name -> KindVar
-- Use the specified name; don't clone it
mkKindSigVar n = mkTcTyVar n superKind (SkolemTv False)
135
\end{code}
136 137


138 139
%************************************************************************
%*									*
140
     Evidence variables; range over constraints we can abstract over
141 142 143 144
%*									*
%************************************************************************

\begin{code}
145 146 147 148
newEvVars :: TcThetaType -> TcM [EvVar]
newEvVars theta = mapM newEvVar theta

newWantedEvVar :: TcPredType -> TcM EvVar 
batterseapower's avatar
batterseapower committed
149
newWantedEvVar = newEvVar
150 151 152 153

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

154
--------------
batterseapower's avatar
batterseapower committed
155

156 157
newEvVar :: TcPredType -> TcM EvVar
-- Creates new *rigid* variables for predicates
158
newEvVar ty = do { name <- newSysName (predTypeOccName ty) 
batterseapower's avatar
batterseapower committed
159
                 ; return (mkLocalId name ty) }
160

batterseapower's avatar
batterseapower committed
161 162
newEq :: TcType -> TcType -> TcM EvVar
newEq ty1 ty2
163
  = do { name <- newSysName (mkVarOccFS (fsLit "cobox"))
164
       ; return (mkLocalId name (mkTcEqPred ty1 ty2)) }
165 166 167

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

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


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

186
\begin{code}
187
tcInstType :: ([TyVar] -> TcM (TvSubst, [TcTyVar]))     -- How to instantiate the type variables
188 189 190 191 192 193 194 195 196 197
	   -> 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)
198

199 200
	(tyvars, rho) -> do { (subst, tyvars') <- inst_tyvars tyvars
			    ; let (theta, tau) = tcSplitPhiTy (substTy subst rho)
201
			    ; return (tyvars', theta, tau) }
202

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

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

tcSuperSkolTyVar :: TvSubst -> TyVar -> (TvSubst, TcTyVar)
tcSuperSkolTyVar subst tv
  = (extendTvSubst subst tv (mkTyVarTy new_tv), new_tv)
dreixel's avatar
dreixel committed
219
  where
220 221 222 223
    kind   = substTy subst (tyVarKind tv)
    new_tv = mkTcTyVar (tyVarName tv) kind superSkolemTv

tcInstSkolTyVar :: Bool -> TvSubst -> TyVar -> TcM (TvSubst, TcTyVar)
224
-- Instantiate the tyvar, using 
225 226 227
--      * the occ-name and kind of the supplied tyvar, 
--      * the unique from the monad,
--      * the location either from the tyvar (skol_info = SigSkol)
228
--                     or from the monad (otherwise)
dreixel's avatar
dreixel committed
229
tcInstSkolTyVar overlappable subst tyvar
230 231 232 233 234
  = 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) }
235 236 237
  where
    old_name = tyVarName tyvar
    occ      = nameOccName old_name
dreixel's avatar
dreixel committed
238
    kind     = substTy subst (tyVarKind tyvar)
239

240
-- Wrappers
241 242 243 244
tcInstSkolTyVars :: [TyVar] -> TcM (TvSubst, [TcTyVar])
tcInstSkolTyVars = tcInstSkolTyVarsX (mkTopTvSubst [])

tcInstSuperSkolTyVars :: [TyVar] -> TcM [TcTyVar]
245
tcInstSuperSkolTyVars = fmap snd . tcInstSkolTyVars' True  (mkTopTvSubst [])
dreixel's avatar
dreixel committed
246

247 248 249 250
tcInstSkolTyVarsX, tcInstSuperSkolTyVarsX
  :: TvSubst -> [TyVar] -> TcM (TvSubst, [TcTyVar])
tcInstSkolTyVarsX      subst = tcInstSkolTyVars' False subst
tcInstSuperSkolTyVarsX subst = tcInstSkolTyVars' True  subst
251

252 253 254 255 256
tcInstSkolTyVars' :: Bool -> TvSubst -> [TyVar] -> TcM (TvSubst, [TcTyVar])
-- Precondition: tyvars should be ordered (kind vars first)
-- see Note [Kind substitution when instantiating]
tcInstSkolTyVars' isSuperSkol = mapAccumLM (tcInstSkolTyVar isSuperSkol)

257
tcInstSkolType :: TcType -> TcM ([TcTyVar], TcThetaType, TcType)
258 259
-- Instantiate a type with fresh skolem constants
-- Binding location comes from the monad
260
tcInstSkolType ty = tcInstType tcInstSkolTyVars ty
261

262
tcInstSigTyVars :: [TyVar] -> TcM (TvSubst, [TcTyVar])
263 264
-- 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
265 266
-- Precondition: tyvars should be ordered (kind vars first)
-- see Note [Kind substitution when instantiating]
267 268 269
tcInstSigTyVars = mapAccumLM tcInstSigTyVar (mkTopTvSubst [])
	-- The tyvars are freshly made, by tcInstSigTyVar
        -- So mkTopTvSubst [] is ok
270 271 272

tcInstSigTyVar :: TvSubst -> TyVar -> TcM (TvSubst, TcTyVar)
tcInstSigTyVar subst tv
273 274 275 276 277
  = do { new_tv <- newSigTyVar (tyVarName tv) (substTy subst (tyVarKind tv))
       ; return (extendTvSubst subst tv (mkTyVarTy new_tv), new_tv) }

newSigTyVar :: Name -> Kind -> TcM TcTyVar
newSigTyVar name kind
278
  = do { uniq <- newUnique
279
       ; let name' = setNameUnique name uniq
280
                      -- Use the same OccName so that the tidy-er
281
                      -- doesn't gratuitously rename 'a' to 'a0' etc
282 283 284 285 286 287 288 289
       ; details <- newMetaDetails SigTv
       ; return (mkTcTyVar name' kind details) }

newMetaDetails :: MetaInfo -> TcM TcTyVarDetails
newMetaDetails info 
  = do { ref <- newMutVar Flexi
       ; untch <- getUntouchables
       ; return (MetaTv { mtv_info = info, mtv_ref = ref, mtv_untch = untch }) }
290 291
\end{code}

dreixel's avatar
dreixel committed
292 293 294 295 296 297 298 299 300 301 302 303 304 305 306
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)]

307 308 309

%************************************************************************
%*									*
310
	MetaTvs (meta type variables; mutable)
311 312 313 314
%*									*
%************************************************************************

\begin{code}
315
newMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar
316
-- Make a new meta tyvar out of thin air
317
newMetaTyVar meta_info kind
318
  = do	{ uniq <- newUnique
319 320
        ; let name = mkTcTyVarName uniq s
              s = case meta_info of
Simon Peyton Jones's avatar
Simon Peyton Jones committed
321 322
                        TauTv -> fsLit "t"
                        SigTv -> fsLit "a"
323 324
        ; details <- newMetaDetails meta_info
	; return (mkTcTyVar name kind details) }
325

326 327 328 329 330 331 332 333 334 335 336
cloneMetaTyVar :: TcTyVar -> TcM TcTyVar
cloneMetaTyVar tv
  = ASSERT( isTcTyVar tv )
    do	{ uniq <- newUnique
        ; ref  <- newMutVar Flexi
        ; let name'    = setNameUnique (tyVarName tv) uniq
              details' = case tcTyVarDetails tv of 
                           details@(MetaTv {}) -> details { mtv_ref = ref }
                           _ -> pprPanic "cloneMetaTyVar" (ppr tv)
        ; return (mkTcTyVar name' (tyVarKind tv) details') }

337 338 339 340 341
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
342
-- Works for both type and kind variables
343 344 345 346
readMetaTyVar :: TyVar -> TcM MetaDetails
readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
		      readMutVar (metaTvRef tyvar)

347 348 349 350
isFilledMetaTyVar :: TyVar -> TcM Bool
-- True of a filled-in (Indirect) meta type variable
isFilledMetaTyVar tv
  | not (isTcTyVar tv) = return False
351
  | MetaTv { mtv_ref = ref } <- tcTyVarDetails tv
352 353 354 355
  = do 	{ details <- readMutVar ref
	; return (isIndirect details) }
  | otherwise = return False

356 357 358 359
isFlexiMetaTyVar :: TyVar -> TcM Bool
-- True of a un-filled-in (Flexi) meta type variable
isFlexiMetaTyVar tv
  | not (isTcTyVar tv) = return False
360
  | MetaTv { mtv_ref = ref } <- tcTyVarDetails tv
361 362 363 364 365
  = do 	{ details <- readMutVar ref
	; return (isFlexi details) }
  | otherwise = return False

--------------------
dreixel's avatar
dreixel committed
366
-- Works with both type and kind variables
367
writeMetaTyVar :: TcTyVar -> TcType -> TcM ()
368 369
-- Write into a currently-empty MetaTyVar

Ian Lynagh's avatar
Ian Lynagh committed
370
writeMetaTyVar tyvar ty
371 372 373 374 375 376 377 378
  | 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 ()

379
  | MetaTv { mtv_ref = ref } <- tcTyVarDetails tyvar
380 381 382 383
  = writeMetaTyVarRef tyvar ref ty

  | otherwise
  = WARN( True, text "Writing to non-meta tyvar" <+> ppr tyvar )
384
    return ()
385 386 387 388 389 390 391 392 393 394 395

--------------------
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
396
  | otherwise
397
  = do { meta_details <- readMutVar ref; 
dreixel's avatar
dreixel committed
398 399 400 401 402
       -- 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
403 404
       ; ASSERT2( isFlexi meta_details, 
                  hang (text "Double update of meta tyvar")
405 406 407
                   2 (ppr tyvar $$ ppr meta_details) )

         traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
dreixel's avatar
dreixel committed
408 409 410
       ; writeMutVar ref (Indirect ty) 
       ; when (   not (isPredTy tv_kind) 
                    -- Don't check kinds for updates to coercion variables
411
               && not (zonked_ty_kind `tcIsSubKind` zonked_tv_kind))
dreixel's avatar
dreixel committed
412 413 414 415 416
       $ 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 ()) }
417 418 419
  where
    tv_kind = tyVarKind tyvar
    ty_kind = typeKind ty
420 421
\end{code}

422 423 424 425 426 427 428 429 430 431 432 433

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

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

newFlexiTyVarTy  :: Kind -> TcM TcType
434 435 436
newFlexiTyVarTy kind = do
    tc_tyvar <- newFlexiTyVar kind
    return (TyVarTy tc_tyvar)
437 438

newFlexiTyVarTys :: Int -> Kind -> TcM [TcType]
439
newFlexiTyVarTys n kind = mapM newFlexiTyVarTy (nOfThem n kind)
440

441
tcInstTyVars :: [TKVar] -> TcM ([TcTyVar], [TcType], TvSubst)
442
-- Instantiate with META type variables
443 444 445
-- Note that this works for a sequence of kind and type
-- variables.  Eg    [ (k:BOX), (a:k->k) ]
--             Gives [ (k7:BOX), (a8:k7->k7) ]
dreixel's avatar
dreixel committed
446 447 448 449 450
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.

451 452
tcInstTyVarsX :: TvSubst -> [TKVar] -> TcM ([TcTyVar], [TcType], TvSubst)
-- The "X" part is because of extending the substitution
dreixel's avatar
dreixel committed
453
tcInstTyVarsX subst tyvars =
454
  do { (subst', tyvars') <- mapAccumLM tcInstTyVarX subst tyvars
dreixel's avatar
dreixel committed
455 456
     ; return (tyvars', mkTyVarTys tyvars', subst') }

457
tcInstTyVarX :: TvSubst -> TKVar -> TcM (TvSubst, TcTyVar)
dreixel's avatar
dreixel committed
458 459
-- Make a new unification variable tyvar whose Name and Kind come from
-- an existing TyVar. We substitute kind variables in the kind.
460
tcInstTyVarX subst tyvar
461 462
  = do  { uniq <- newUnique
        ; details <- newMetaDetails TauTv
dreixel's avatar
dreixel committed
463 464
        ; let name   = mkSystemName uniq (getOccName tyvar)
              kind   = substTy subst (tyVarKind tyvar)
465
              new_tv = mkTcTyVar name kind details 
dreixel's avatar
dreixel committed
466
        ; return (extendTvSubst subst tyvar (mkTyVarTy new_tv), new_tv) }
467 468 469 470 471
\end{code}


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

476 477 478
@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.
479 480

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

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

\begin{code}
494 495 496 497 498 499 500 501 502 503 504 505
zonkTyVar :: TyVar -> TcM TcType
-- Works on TyVars and TcTyVars
zonkTyVar tv | isTcTyVar tv = zonkTcTyVar tv
             | otherwise    = return (mkTyVarTy tv)
   -- Hackily, when typechecking type and class decls
   -- we have TyVars in scopeadded (only) in 
   -- TcHsType.tcTyClTyVars, but it seems
   -- painful to make them into TcTyVars there

zonkTyVarsAndFV :: TyVarSet -> TcM TyVarSet
zonkTyVarsAndFV tyvars = tyVarsOfTypes <$> mapM zonkTyVar (varSetElems tyvars)

506
zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
507
zonkTcTyVars tyvars = mapM zonkTcTyVar tyvars
508 509

-----------------  Types
dreixel's avatar
dreixel committed
510 511 512
zonkTyVarKind :: TyVar -> TcM TyVar
zonkTyVarKind tv = do { kind' <- zonkTcKind (tyVarKind tv)
                      ; return (setTyVarKind tv kind') }
513

514
zonkTcTypes :: [TcType] -> TcM [TcType]
515
zonkTcTypes tys = mapM zonkTcType tys
516

517
zonkTcThetaType :: TcThetaType -> TcM TcThetaType
518
zonkTcThetaType theta = mapM zonkTcPredType theta
519

520
zonkTcPredType :: TcPredType -> TcM TcPredType
batterseapower's avatar
batterseapower committed
521
zonkTcPredType = zonkTcType
522 523 524 525 526 527
\end{code}

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

\begin{code}
dreixel's avatar
dreixel committed
528
defaultKindVarToStar :: TcTyVar -> TcM Kind
dreixel's avatar
dreixel committed
529 530
-- We have a meta-kind: unify it with '*'
defaultKindVarToStar kv 
531
  = do { ASSERT ( isKindVar kv && isMetaTyVar kv )
dreixel's avatar
dreixel committed
532 533
         writeMetaTyVar kv liftedTypeKind
       ; return liftedTypeKind }
dreixel's avatar
dreixel committed
534

535
zonkQuantifiedTyVars :: [TcTyVar] -> TcM [TcTyVar]
536
-- A kind variable k may occur *after* a tyvar mentioning k in its kind
dreixel's avatar
dreixel committed
537
zonkQuantifiedTyVars tyvars
538
  = do { let (kvs, tvs) = partition isKindVar tyvars
dreixel's avatar
dreixel committed
539 540 541 542 543 544 545 546 547 548 549 550 551 552 553
       ; 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) } }
554

555
zonkQuantifiedTyVar :: TcTyVar -> TcM TcTyVar
556 557 558 559
-- 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
560
-- The meta tyvar is updated to point to the new skolem TyVar.  Now any 
561 562 563
-- bound occurences of the original type variable will get zonked to 
-- the immutable version.
--
564
-- We leave skolem TyVars alone; they are immutable.
dreixel's avatar
dreixel committed
565 566 567
--
-- This function is called on both kind and type variables,
-- but kind variables *only* if PolyKinds is on.
568
zonkQuantifiedTyVar tv
569 570
  = ASSERT2( isTcTyVar tv, ppr tv ) 
    case tcTyVarDetails tv of
dreixel's avatar
dreixel committed
571
      SkolemTv {} -> do { kind <- zonkTcKind (tyVarKind tv)
572
                        ; return $ setTyVarKind tv kind }
573 574 575
	-- It might be a skolem type variable, 
	-- for example from a user type signature

576
      MetaTv { mtv_ref = ref } ->
Ian Lynagh's avatar
Ian Lynagh committed
577 578 579 580 581 582 583 584 585
          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
586 587 588
      _other -> pprPanic "zonkQuantifiedTyVar" (ppr tv) -- FlatSkol, RuntimeUnk

skolemiseUnboundMetaTyVar :: TcTyVar -> TcTyVarDetails -> TcM TyVar
589 590 591 592 593
-- 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]
594
skolemiseUnboundMetaTyVar tv details
595
  = ASSERT2( isMetaTyVar tv, ppr tv ) 
596 597 598
    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
599 600
        ; kind <- zonkTcKind (tyVarKind tv)
        ; let final_kind = defaultKind kind
601 602
              final_name = mkInternalName uniq (getOccName tv) span
              final_tv   = mkTcTyVar final_name final_kind details
dreixel's avatar
dreixel committed
603 604 605

        ; writeMetaTyVar tv (mkTyVarTy final_tv)
        ; return final_tv }
606 607 608 609 610 611 612 613 614 615 616

skolemiseSigTv :: TcTyVar -> TcM TcTyVar
-- In TcBinds we create SigTvs for type signatures
-- but for singleton groups we want them to really be skolems
-- which do not unify with each other
skolemiseSigTv tv  
  = ASSERT2( isSigTyVar tv, ppr tv )
    do { writeMetaTyVarRef tv (metaTvRef tv) (mkTyVarTy skol_tv)
       ; return skol_tv }
  where
    skol_tv = setTcTyVarDetails tv (SkolemTv False)
617 618
\end{code}

619 620
\begin{code}
zonkImplication :: Implication -> TcM Implication
621 622
zonkImplication implic@(Implic { ic_untch  = untch
                               , ic_binds  = binds_var
623
                               , ic_skols  = skols
624
                               , ic_given  = given
625
                               , ic_wanted = wanted
626
                               , ic_info   = info })
627 628
  = do { skols'  <- mapM zonkTcTyVarBndr skols  -- Need to zonk their kinds!
                                                -- as Trac #7230 showed
629
       ; given'  <- mapM zonkEvVar given
630
       ; info'   <- zonkSkolemInfo info
631
       ; wanted' <- zonkWCRec binds_var untch wanted
632 633
       ; return (implic { ic_skols = skols'
                        , ic_given = given'
634
                        , ic_fsks  = []  -- Zonking removes all FlatSkol tyvars
635
                        , ic_wanted = wanted'
636
                        , ic_info = info' }) }
637 638 639 640 641

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

642

643 644 645
zonkWC :: EvBindsVar -- May add new bindings for wanted family equalities in here
       -> WantedConstraints -> TcM WantedConstraints
zonkWC binds_var wc
646 647
  = do { untch <- getUntouchables
       ; zonkWCRec binds_var untch wc }
648 649 650 651 652 653

zonkWCRec :: EvBindsVar
          -> Untouchables
          -> WantedConstraints -> TcM WantedConstraints
zonkWCRec binds_var untch (WC { wc_flat = flat, wc_impl = implic, wc_insol = insol })
  = do { flat'   <- zonkFlats binds_var untch flat
654
       ; implic' <- mapBagM zonkImplication implic
655
       ; insol'  <- zonkCts insol -- No need to do the more elaborate zonkFlats thing
656 657
       ; return (WC { wc_flat = flat', wc_impl = implic', wc_insol = insol' }) }

658 659 660
zonkFlats :: EvBindsVar -> Untouchables -> Cts -> TcM Cts
-- This zonks and unflattens a bunch of flat constraints
-- See Note [Unflattening while zonking]
661 662 663 664
zonkFlats binds_var untch cts
  = do { -- See Note [How to unflatten]
         cts <- foldrBagM unflatten_one emptyCts cts
       ; zonkCts cts }
665 666
  where
    unflatten_one orig_ct cts
667 668
      = do { zct <- zonkCt orig_ct                -- First we need to fully zonk 
           ; mct <- try_zonk_fun_eq orig_ct zct   -- Then try to solve if family equation
669
           ; return $ maybe cts (`consBag` cts) mct }
670 671 672 673 674 675 676 677 678 679 680 681

    try_zonk_fun_eq orig_ct zct   -- See Note [How to unflatten]
      | EqPred ty_lhs ty_rhs <- classifyPredType (ctPred zct)
          -- NB: zonking de-classifies the constraint,
          --     so we can't look for CFunEqCan
      , Just tv <- getTyVar_maybe ty_rhs
      , ASSERT2( not (isFloatedTouchableMetaTyVar untch tv), ppr tv )
        isTouchableMetaTyVar untch tv
      , typeKind ty_lhs `tcIsSubKind` tyVarKind tv
      , not (tv `elemVarSet` tyVarsOfType ty_lhs)
--       , Just ty_lhs' <- occurCheck tv ty_lhs
      = ASSERT2( isWantedCt orig_ct, ppr orig_ct )
Simon Peyton Jones's avatar
Simon Peyton Jones committed
682
        ASSERT2( case tcSplitTyConApp_maybe ty_lhs of { Just (tc,_) -> isSynFamilyTyCon tc; _ -> False }, ppr orig_ct )
683 684 685 686 687 688 689 690 691 692
        do { writeMetaTyVar tv ty_lhs
           ; let evterm = EvCoercion (mkTcReflCo ty_lhs)
                 evvar  = ctev_evar (cc_ev zct)
           ; addTcEvBind binds_var evvar evterm
           ; traceTc "zonkFlats/unflattening" $
             vcat [ text "zct = " <+> ppr zct,
                    text "binds_var = " <+> ppr binds_var ]
           ; return Nothing }
      | otherwise
      = return (Just zct)
693 694 695 696 697 698 699 700 701 702 703 704
\end{code}

Note [Unflattening while zonking]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
A bunch of wanted constraints could contain wanted equations of the form
(F taus ~ alpha) where alpha is either an ordinary unification variable, or
a flatten unification variable.

These are ordinary wanted constraints and can/should be solved by
ordinary unification alpha := F taus. However the constraint solving
algorithm does not do that, as their 'inert' form is F taus ~ alpha.

705
Hence, we need an extra step to 'unflatten' these equations by
706 707 708 709 710 711 712 713 714
performing unification. This unification, if it happens at the end of
constraint solving, cannot produce any more interactions in the
constraint solver so it is safe to do it as the very very last step.

We choose therefore to do it during zonking, in the function
zonkFlats. This is in analgoy to the zonking of given flatten skolems
which are eliminated in favor of the underlying type that they are
equal to.

715
Note that, because we now have to affect *evidence* while zonking
716 717 718 719
(setting some evidence binds to identities), we have to pass to the
zonkWC function an evidence variable to collect all the extra
variables.

720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738
Note [How to unflatten]
~~~~~~~~~~~~~~~~~~~~~~~
How do we unflatten during zonking.  Consider a bunch of flat constraints.
Consider them one by one.  For each such constraint C
  * Zonk C (to apply current substitution)
  * If C is of form F tys ~ alpha, 
       where alpha is touchable
       and   alpha is not mentioned in tys
    then unify alpha := F tys
         and discard C

After processing all the flat constraints, zonk them again to propagate
the inforamtion from later ones to earlier ones.  Eg
  Start:  (F alpha ~ beta, G Int ~ alpha)
  Then we get beta := F alpha
              alpha := G Int
  but we must apply the second unification to the first constraint.


739
\begin{code}
740 741 742
zonkCts :: Cts -> TcM Cts
zonkCts = mapBagM zonkCt

743
zonkCt :: Ct -> TcM Ct
744 745 746
zonkCt ct@(CHoleCan { cc_ev = ev })
  = do { ev' <- zonkCtEvidence ev
       ; return $ ct { cc_ev = ev' } }
747
zonkCt ct
748 749 750
  = do { fl' <- zonkCtEvidence (cc_ev ct)
       ; return (CNonCanonical { cc_ev = fl'
                               , cc_loc = cc_loc ct }) }
751

752
zonkCtEvidence :: CtEvidence -> TcM CtEvidence
753 754 755
zonkCtEvidence ctev@(CtGiven { ctev_pred = pred }) 
  = do { pred' <- zonkTcType pred
       ; return (ctev { ctev_pred = pred'}) }
Simon Peyton Jones's avatar
Simon Peyton Jones committed
756
zonkCtEvidence ctev@(CtWanted { ctev_pred = pred })
757 758
  = do { pred' <- zonkTcType pred
       ; return (ctev { ctev_pred = pred' }) }
Simon Peyton Jones's avatar
Simon Peyton Jones committed
759
zonkCtEvidence ctev@(CtDerived { ctev_pred = pred })
760 761
  = do { pred' <- zonkTcType pred
       ; return (ctev { ctev_pred = pred' }) }
762 763 764 765 766 767 768 769 770

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
771 772
\end{code}

773 774
Note [Silly Type Synonyms]
~~~~~~~~~~~~~~~~~~~~~~~~~~
775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 791
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
792
  because it does not 'really' mention a.  (see exactTyVarsOfType)
793
  The arg to foo becomes
Ian Lynagh's avatar
Ian Lynagh committed
794
	\/\a -> \t -> t+t
795 796 797

* So we get a dict binding for Num (C d a), which is zonked to give
	a = ()
798 799 800 801
  [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!]
802

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

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

808 809 810 811 812 813 814 815 816 817 818
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

819
It leads to the deferral of an equality (wrapped in an implication constraint)
820

dreixel's avatar
dreixel committed
821
  forall a. () => ((String -> String -> String) ~ a)
822 823 824 825 826 827 828 829 830 831 832 833 834 835

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
836
(which we require for a quantified variable), but is still a TcTyVar that the
837 838
simplifier knows how to deal with.

839 840 841

%************************************************************************
%*									*
842
\subsection{Zonking -- the main work-horses: zonkTcType, zonkTcTyVar}
843 844 845 846 847 848
%*									*
%*		For internal use only!					*
%*									*
%************************************************************************

\begin{code}
849 850 851 852 853 854
-- zonkId is used *during* typechecking just to zonk the Id's type
zonkId :: TcId -> TcM TcId
zonkId id
  = do { ty' <- zonkTcType (idType id)
       ; return (Id.setIdType id ty') }

855 856 857 858
-- 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

859 860
zonkTcType :: TcType -> TcM TcType
zonkTcType ty
861 862
  = go ty
  where
863 864 865
    go (TyConApp tc tys) = do tys' <- mapM go tys
                              return (TyConApp tc tys')

866
    go (LitTy n)         = return (LitTy n)
867

868 869 870 871 872 873 874
    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')
875 876 877
		-- NB the mkAppTy; we might have instantiated a
		-- type variable to a type constructor, so we need
		-- to pull the TyConApp to the top.
878 879

	-- The two interesting cases!
880
    go (TyVarTy tyvar) | isTcTyVar tyvar = zonkTcTyVar tyvar
881
		       | otherwise	 = TyVarTy <$> updateTyVarKindM go tyvar
882
		-- Ordinary (non Tc) tyvars occur inside quantified types
883

884 885 886 887 888 889 890 891 892 893 894 895
    go (ForAllTy tv ty) = do { tv' <- zonkTcTyVarBndr tv
                             ; ty' <- go ty
                             ; return (ForAllTy tv' ty') }

zonkTcTyVarBndr :: TcTyVar -> TcM TcTyVar
-- A tyvar binder is never a unification variable (MetaTv),
-- rather it is always a skolems.  BUT it may have a kind 
-- that has not yet been zonked, and may include kind
-- unification variables.
zonkTcTyVarBndr tyvar
  = ASSERT2( isImmutableTyVar tyvar, ppr tyvar ) do
    updateTyVarKindM zonkTcType tyvar
896 897 898 899 900 901 902 903 904

zonkTcTyVar :: TcTyVar -> TcM TcType
-- Simply look through all Flexis
zonkTcTyVar tv
  = ASSERT2( isTcTyVar tv, ppr tv ) do
    case tcTyVarDetails tv of
      SkolemTv {}   -> zonk_kind_and_return
      RuntimeUnk {} -> zonk_kind_and_return
      FlatSkol ty   -> zonkTcType ty
905 906 907 908 909
      MetaTv { mtv_ref = ref }
         -> do { cts <- readMutVar ref
               ; case cts of
	            Flexi       -> zonk_kind_and_return
	            Indirect ty -> zonkTcType ty }
910 911 912
  where
    zonk_kind_and_return = do { z_tv <- zonkTyVarKind tv
                              ; return (TyVarTy z_tv) }
913 914 915 916
\end{code}



917 918 919 920 921 922 923 924
%************************************************************************
%*									*
			Zonking kinds
%*									*
%************************************************************************

\begin{code}
zonkTcKind :: TcKind -> TcM TcKind
925
zonkTcKind k = zonkTcType k
926 927
\end{code}
			
928 929
%************************************************************************
%*									*
930 931 932 933 934 935 936 937 938
\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,
939 940
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.
941 942 943 944 945 946 947 948 949 950 951 952 953 954

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
	
955 956 957 958 959
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!
960

961
	
962
\begin{code}
963 964 965 966 967 968 969 970 971 972 973 974 975 976 977 978 979
check_kind :: UserTypeCtxt -> TcType -> TcM ()
-- Check that the type's kind is acceptable for the context
check_kind ctxt ty
  | TySynCtxt {} <- ctxt
  = do { ck <- xoptM Opt_ConstraintKinds
       ; unless ck $
         checkTc (not (returnsConstraintKind actual_kind)) 
                 (constraintSynErr actual_kind) }

  | Just k <- expectedKindInCtxt ctxt
  = checkTc (tcIsSubKind actual_kind k) (kindErr actual_kind)

  | otherwise
  = return ()   -- Any kind will do
  where
    actual_kind = typeKind ty

980 981 982 983 984 985 986
-- 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 (ForSigCtxt _) = Just liftedTypeKind
987 988
expectedKindInCtxt InstDeclCtxt   = Just constraintKind
expectedKindInCtxt SpecInstCtxt   = Just constraintKind
989
expectedKindInCtxt _              = Just openTypeKind
990

991 992
checkValidType :: UserTypeCtxt -> Type -> TcM ()
-- Checks that the type is valid for the given context
993 994 995
-- Not used for instance decls; checkValidInstance instead
checkValidType ctxt ty 
  = do { traceTc "checkValidType" (ppr ty <+> text "::" <+> ppr (typeKind ty))
996 997
       ; rank2_flag      <- xoptM Opt_Rank2Types
       ; rankn_flag      <- xoptM Opt_RankNTypes
998
       ; polycomp        <- xoptM Opt_PolymorphicComponents
999 1000 1001 1002 1003 1004 1005 1006 1007 1008 1009 1010 1011 1012
       ; let gen_rank :: Rank -> Rank
             gen_rank r | rankn_flag = ArbitraryRank
	                | rank2_flag = r2
	                | otherwise  = r

             rank2 = gen_rank r2
             rank1 = gen_rank r1
             rank0 = gen_rank r0

             r0 = rankZeroMonoType
             r1 = LimitedRank True r0
             r2 = LimitedRank True r1

             rank
1013 1014 1015
	       = case ctxt of
	     	 DefaultDeclCtxt-> MustBeMonoType
	     	 ResSigCtxt	-> MustBeMonoType
1016 1017
	     	 LamPatSigCtxt	-> rank0
	     	 BindPatSigCtxt	-> rank0
1018
	     	 RuleSigCtxt _  -> rank1
1019
	     	 TySynCtxt _    -> rank0
1020

1021 1022
	     	 ExprSigCtxt 	-> rank1
	     	 FunSigCtxt _   -> rank1
1023
	     	 InfSigCtxt _   -> ArbitraryRank	-- Inferred type
1024
	     	 ConArgCtxt _   | polycomp -> rank2
1025 1026
                                     -- We are given the type of the entire
                                     -- constructor, hence rank 1
1027
 	     			| otherwise -> rank1
1028

1029 1030 1031
	     	 ForSigCtxt _	-> rank1
	     	 SpecInstCtxt   -> rank1
                 ThBrackCtxt    -> rank1
1032
	     	 GhciCtxt       -> ArbitraryRank
dreixel's avatar
dreixel committed
1033
                 _              -> panic "checkValidType"
1034
                                          -- Can't happen; not used for *user* sigs
1035 1036

	-- Check the internal validity of the type itself