TcType.hs 91.3 KB
Newer Older
Austin Seipp's avatar
Austin Seipp committed
1 2 3 4
{-
(c) The University of Glasgow 2006
(c) The GRASP/AQUA Project, Glasgow University, 1992-1998

5 6
\section[TcType]{Types used in the typechecker}

7 8
This module provides the Type interface for front-end parts of the
compiler.  These parts
9

10 11 12
        * treat "source types" as opaque:
                newtypes, and predicates are meaningful.
        * look through usage types
13

14
The "tc" prefix is for "TypeChecker", because the type checker
15
is the principal client.
Austin Seipp's avatar
Austin Seipp committed
16
-}
17

18
{-# LANGUAGE CPP, MultiWayIf #-}
19

20
module TcType (
21
  --------------------------------
22 23
  -- Types
  TcType, TcSigmaType, TcRhoType, TcTauType, TcPredType, TcThetaType,
24
  TcTyVar, TcTyVarSet, TcDTyVarSet, TcTyCoVarSet, TcDTyCoVarSet,
Simon Peyton Jones's avatar
Simon Peyton Jones committed
25
  TcKind, TcCoVar, TcTyCoVar, TcTyVarBinder, TcTyCon,
26

27
  ExpType(..), InferResult(..), ExpSigmaType, ExpRhoType, mkCheckExpType,
28 29 30

  SyntaxOpType(..), synKnownType, mkSynFunTys,

31
  -- TcLevel
32
  TcLevel(..), topTcLevel, pushTcLevel, isTopTcLevel,
33
  strictlyDeeperThan, sameDepthAs, fmvTcLevel,
34
  tcTypeLevel, tcTyVarLevel, maxTcLevel,
35

36
  --------------------------------
37
  -- MetaDetails
38
  UserTypeCtxt(..), pprUserTypeCtxt, isSigMaybe,
39
  TcTyVarDetails(..), pprTcTyVarDetails, vanillaSkolemTv, superSkolemTv,
40
  MetaDetails(Flexi, Indirect), MetaInfo(..),
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
41
  isImmutableTyVar, isSkolemTyVar, isMetaTyVar,  isMetaTyVarTy, isTyVarTy,
Austin Seipp's avatar
Austin Seipp committed
42
  isSigTyVar, isOverlappableTyVar,  isTyConableTyVar,
43
  isFskTyVar, isFmvTyVar, isFlattenTyVar,
44
  isAmbiguousTyVar, metaTyVarRef, metaTyVarInfo,
45
  isFlexi, isIndirect, isRuntimeUnkSkol,
46
  metaTyVarTcLevel, setMetaTyVarTcLevel, metaTyVarTcLevel_maybe,
47 48
  isTouchableMetaTyVar, isTouchableOrFmv,
  isFloatedTouchableMetaTyVar,
49 50

  --------------------------------
51
  -- Builders
52
  mkPhiTy, mkInfSigmaTy, mkSpecSigmaTy, mkSigmaTy,
53 54
  mkNakedTyConApp, mkNakedAppTys, mkNakedAppTy,
  mkNakedCastTy,
55

56
  --------------------------------
57
  -- Splitters
58
  -- These are important because they do not look through newtypes
59
  getTyVar,
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
60
  tcSplitForAllTy_maybe,
Simon Peyton Jones's avatar
Simon Peyton Jones committed
61
  tcSplitForAllTys, tcSplitPiTys, tcSplitForAllTyVarBndrs,
62
  tcSplitPhiTy, tcSplitPredFunTy_maybe,
63
  tcSplitFunTy_maybe, tcSplitFunTys, tcFunArgTy, tcFunResultTy, tcSplitFunTysN,
64 65 66
  tcSplitTyConApp, tcSplitTyConApp_maybe, tcRepSplitTyConApp_maybe,
  tcTyConAppTyCon, tcTyConAppArgs,
  tcSplitAppTy_maybe, tcSplitAppTy, tcSplitAppTys, tcRepSplitAppTy_maybe,
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
67
  tcGetTyVar_maybe, tcGetTyVar, nextRole,
68
  tcSplitSigmaTy, tcDeepSplitSigmaTy_maybe,
69 70

  ---------------------------------
71
  -- Predicates.
72
  -- Again, newtypes are opaque
niteria's avatar
niteria committed
73
  eqType, eqTypes, nonDetCmpType, nonDetCmpTypes, eqTypeX,
74
  pickyEqType, tcEqType, tcEqKind, tcEqTypeNoKindCheck, tcEqTypeVis,
75
  isSigmaTy, isRhoTy, isRhoExpTy, isOverloadedTy,
Ben Gamari's avatar
Ben Gamari committed
76
  isFloatingTy, isDoubleTy, isFloatTy, isIntTy, isWordTy, isStringTy,
Eric Seidel's avatar
Eric Seidel committed
77
  isIntegerTy, isBoolTy, isUnitTy, isCharTy, isCallStackTy, isCallStackPred,
78
  isTauTy, isTauTyCon, tcIsTyVarTy, tcIsForAllTy,
79
  isPredTy, isTyVarClassPred, isTyVarExposed, isTyVarUnderDatatype,
80
  checkValidClsArgs, hasTyVarHead,
81
  isRigidEqPred, isRigidTy,
82

83 84
  ---------------------------------
  -- Misc type manipulators
85 86

  deNoteType,
Simon Peyton Jones's avatar
Simon Peyton Jones committed
87
  orphNamesOfType, orphNamesOfCo,
88
  orphNamesOfTypes, orphNamesOfCoCon,
89
  getDFunTyKey,
90
  evVarPred_maybe, evVarPred,
91 92

  ---------------------------------
93
  -- Predicate types
94
  mkMinimalBySCs, transSuperClasses,
95
  pickQuantifiablePreds, pickCapturedPreds,
96 97
  immSuperClasses,
  isImprovementPred,
98

99 100 101 102
  -- * Finding type instances
  tcTyFamInsts,

  -- * Finding "exact" (non-dead) type variables
103
  exactTyCoVarsOfType, exactTyCoVarsOfTypes,
104
  splitDepVarsOfType, splitDepVarsOfTypes, TcDepVars(..), tcDepVarSet,
105
  rewritableTyVarsOfTypes, rewritableTyVarsOfType,
106 107 108

  -- * Extracting bound variables
  allBoundVariables, allBoundVariabless,
109

110 111 112 113 114 115
  ---------------------------------
  -- Foreign import and export
  isFFIArgumentTy,     -- :: DynFlags -> Safety -> Type -> Bool
  isFFIImportResultTy, -- :: DynFlags -> Type -> Bool
  isFFIExportResultTy, -- :: Type -> Bool
  isFFIExternalTy,     -- :: Type -> Bool
116
  isFFIDynTy,          -- :: Type -> Type -> Bool
117 118
  isFFIPrimArgumentTy, -- :: DynFlags -> Type -> Bool
  isFFIPrimResultTy,   -- :: DynFlags -> Type -> Bool
119
  isFFILabelTy,        -- :: Type -> Bool
120
  isFFITy,             -- :: Type -> Bool
121
  isFunPtrTy,          -- :: Type -> Bool
122
  tcSplitIOType_maybe, -- :: Type -> Maybe Type
123

124
  --------------------------------
125 126
  -- Rexported from Kind
  Kind, typeKind,
127
  liftedTypeKind,
128 129
  constraintKind,
  isLiftedTypeKind, isUnliftedTypeKind, classifiesTypeWithValues,
130

131 132
  --------------------------------
  -- Rexported from Type
133
  Type, PredType, ThetaType, TyBinder, ArgFlag(..),
134

Simon Peyton Jones's avatar
Simon Peyton Jones committed
135
  mkForAllTy, mkForAllTys, mkInvForAllTys, mkSpecForAllTys, mkInvForAllTy,
136
  mkFunTy, mkFunTys,
137
  mkTyConApp, mkAppTy, mkAppTys,
138 139
  mkTyConTy, mkTyVarTy,
  mkTyVarTys,
140

141
  isClassPred, isEqPred, isNomEqPred, isIPPred,
142
  mkClassPred,
143
  isDictLikeTy,
144
  tcSplitDFunTy, tcSplitDFunHead, tcSplitMethodTy,
145
  isRuntimeRepVar, isLevityPolymorphic,
146
  isVisibleBinder, isInvisibleBinder,
147

148
  -- Type substitutions
149 150
  TCvSubst(..),         -- Representation visible to a few friends
  TvSubstEnv, emptyTCvSubst,
niteria's avatar
niteria committed
151 152
  zipTvSubst,
  mkTvSubstPrs, notElemTCvSubst, unionTCvSubst,
153
  getTvSubstEnv, setTvSubstEnv, getTCvInScope, extendTCvInScope,
154
  extendTCvInScopeList, extendTCvInScopeSet, extendTvSubstAndInScope,
155
  Type.lookupTyVar, Type.extendTCvSubst, Type.substTyVarBndr,
156 157
  Type.extendTvSubst,
  isInScope, mkTCvSubst, mkTvSubst, zipTyEnv, zipCoEnv,
158
  Type.substTy, substTys, substTyWith, substTyWithCoVars,
159 160
  substTyAddInScope,
  substTyUnchecked, substTysUnchecked, substThetaUnchecked,
161
  substTyWithUnchecked,
162
  substCoUnchecked, substCoWithUnchecked,
163
  substTheta,
164

165
  isUnliftedType,       -- Source types are always lifted
166 167
  isUnboxedTupleType,   -- Ditto
  isPrimitiveType,
168

169 170 171
  coreView,

  tyCoVarsOfType, tyCoVarsOfTypes, closeOverKinds,
niteria's avatar
niteria committed
172
  tyCoFVsOfType, tyCoFVsOfTypes,
173 174
  tyCoVarsOfTypeDSet, tyCoVarsOfTypesDSet, closeOverKindsDSet,
  tyCoVarsOfTypeList, tyCoVarsOfTypesList,
175

176 177 178 179 180
  --------------------------------
  -- Transforming Types to TcTypes
  toTcType,    -- :: Type -> TcType
  toTcTypeBag, -- :: Bag EvVar -> Bag EvVar

181
  pprKind, pprParendKind, pprSigmaType,
182
  pprType, pprParendType, pprTypeApp, pprTyThingCategory, tyThingCategory,
183
  pprTheta, pprThetaArrowTy, pprClassPred,
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
184
  pprTvBndr, pprTvBndrs,
185

186
  TypeSize, sizeType, sizeTypes, toposortTyVars
187

188
  ) where
189

190
#include "HsVersions.h"
191

192
-- friends:
193
import Kind
194
import TyCoRep
195 196 197
import Class
import Var
import ForeignCall
198
import VarSet
199
import Coercion
200
import Type
201
import RepType (tyConPrimRep)
202
import TyCon
203 204

-- others:
205
import DynFlags
Simon Peyton Jones's avatar
Simon Peyton Jones committed
206
import CoreFVs
207 208 209
import Name -- hiding (varName)
            -- We use this to make dictionaries for type literals.
            -- Perhaps there's a better way to do this?
210
import NameSet
211 212
import VarEnv
import PrelNames
213 214
import TysWiredIn( coercibleClass, unitTyCon, unitTyConKey
                 , listTyCon, constraintKind )
215 216
import BasicTypes
import Util
217
import Bag
218
import Maybes
219
import Outputable
220
import FastString
221
import ErrUtils( Validity(..), MsgDoc, isValid )
222
import FV
223
import qualified GHC.LanguageExtensions as LangExt
Simon Marlow's avatar
Simon Marlow committed
224 225

import Data.IORef
226
import Data.Functor.Identity
227

Austin Seipp's avatar
Austin Seipp committed
228 229 230
{-
************************************************************************
*                                                                      *
231
              Types
Austin Seipp's avatar
Austin Seipp committed
232 233
*                                                                      *
************************************************************************
234

235
The type checker divides the generic Type world into the
236 237
following more structured beasts:

238
sigma ::= forall tyvars. phi
239 240 241 242
        -- A sigma type is a qualified type
        --
        -- Note that even if 'tyvars' is empty, theta
        -- may not be: e.g.   (?x::Int) => Int
243

244 245 246 247
        -- Note that 'sigma' is in prenex form:
        -- all the foralls are at the front.
        -- A 'phi' type has no foralls to the right of
        -- an arrow
248

249 250 251
phi :: theta => rho

rho ::= sigma -> rho
252 253 254 255 256 257 258 259 260 261 262
     |  tau

-- A 'tau' type has no quantification anywhere
-- Note that the args of a type constructor must be taus
tau ::= tyvar
     |  tycon tau_1 .. tau_n
     |  tau_1 tau_2
     |  tau_1 -> tau_2

-- In all cases, a (saturated) type synonym application is legal,
-- provided it expands to the required form.
Simon Peyton Jones's avatar
Simon Peyton Jones committed
263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298

Note [TcTyVars in the typechecker]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The typechecker uses a lot of type variables with special properties,
notably being a unification variable with a mutable reference.  These
use the 'TcTyVar' variant of Var.Var.

However, the type checker and constraint solver can encounter type
variables that use the 'TyVar' variant of Var.Var, for a couple of
reasons:

  - When unifying or flattening under (forall a. ty)

  - When typechecking a class decl, say
       class C (a :: k) where
          foo :: T a -> Int
    We have first kind-check the header; fix k and (a:k) to be
    TyVars, bring 'k' and 'a' into scope, and kind check the
    signature for 'foo'.  In doing so we call solveEqualities to
    solve any kind equalities in foo's signature.  So the solver
    may see free occurences of 'k'.

It's convenient to simply treat these TyVars as skolem constants,
which of course they are.  So

* Var.tcTyVarDetails succeeds on a TyVar, returning
  vanillaSkolemTv, as well as on a TcTyVar.

* tcIsTcTyVar returns True for both TyVar and TcTyVar variants
  of Var.Var.  The "tc" prefix means "a type variable that can be
  encountered by the typechecker".

This is a bit of a change from an earlier era when we remoselessly
insisted on real TcTyVars in the type checker.  But that seems
unnecessary (for skolems, TyVars are fine) and it's now very hard
to guarantee, with the advent of kind equalities.
Austin Seipp's avatar
Austin Seipp committed
299
-}
300

Simon Peyton Jones's avatar
Simon Peyton Jones committed
301
-- See Note [TcTyVars in the typechecker]
302
type TcTyVar = TyVar    -- Used only during type inference
303
type TcCoVar = CoVar    -- Used only during type inference
304
type TcType = Type      -- A TcType can have mutable type variables
305
type TcTyCoVar = Var    -- Either a TcTyVar or a CoVar
306 307 308 309
        -- Invariant on ForAllTy in TcTypes:
        --      forall a. T
        -- a cannot occur inside a MutTyVar in T; that is,
        -- T is "flattened" before quantifying over a
Simon Peyton Jones's avatar
Simon Peyton Jones committed
310 311 312

type TcTyVarBinder = TyVarBinder
type TcTyCon       = TyCon   -- these can be the TcTyCon constructor
313

314
-- These types do not have boxy type variables in them
315 316
type TcPredType     = PredType
type TcThetaType    = ThetaType
317
type TcSigmaType    = TcType
318
type TcRhoType      = TcType  -- Note [TcRhoType]
319
type TcTauType      = TcType
320
type TcKind         = Kind
321
type TcTyVarSet     = TyVarSet
322
type TcTyCoVarSet   = TyCoVarSet
323
type TcDTyVarSet    = DTyVarSet
324
type TcDTyCoVarSet  = DTyCoVarSet
325

326 327 328 329 330 331 332

{- *********************************************************************
*                                                                      *
          ExpType: an "expected type" in the type checker
*                                                                      *
********************************************************************* -}

333 334 335
-- | An expected type to check against during type-checking.
-- See Note [ExpType] in TcMType, where you'll also find manipulators.
data ExpType = Check TcType
336 337 338 339 340 341 342
             | Infer !InferResult

data InferResult
  = IR { ir_uniq :: Unique  -- For debugging only
       , ir_lvl  :: TcLevel -- See Note [TcLevel of ExpType] in TcMType
       , ir_inst :: Bool    -- True <=> deeply instantiate before returning
                            --           i.e. return a RhoType
Gabor Greif's avatar
Gabor Greif committed
343
                            -- False <=> do not instantiate before returning
344 345
                            --           i.e. return a SigmaType
       , ir_ref  :: IORef (Maybe TcType) }
346 347
         -- The type that fills in this hole should be a Type,
         -- that is, its kind should be (TYPE rr) for some rr
348 349 350 351 352

type ExpSigmaType = ExpType
type ExpRhoType   = ExpType

instance Outputable ExpType where
353 354 355 356 357
  ppr (Check ty) = text "Check" <> braces (ppr ty)
  ppr (Infer ir) = ppr ir

instance Outputable InferResult where
  ppr (IR { ir_uniq = u, ir_lvl = lvl
358
          , ir_inst = inst })
359
    = text "Infer" <> braces (ppr u <> comma <> ppr lvl <+> ppr inst)
360 361 362 363 364

-- | Make an 'ExpType' suitable for checking.
mkCheckExpType :: TcType -> ExpType
mkCheckExpType = Check

365 366 367 368 369 370 371

{- *********************************************************************
*                                                                      *
          SyntaxOpType
*                                                                      *
********************************************************************* -}

372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403
-- | What to expect for an argument to a rebindable-syntax operator.
-- Quite like 'Type', but allows for holes to be filled in by tcSyntaxOp.
-- The callback called from tcSyntaxOp gets a list of types; the meaning
-- of these types is determined by a left-to-right depth-first traversal
-- of the 'SyntaxOpType' tree. So if you pass in
--
-- > SynAny `SynFun` (SynList `SynFun` SynType Int) `SynFun` SynAny
--
-- you'll get three types back: one for the first 'SynAny', the /element/
-- type of the list, and one for the last 'SynAny'. You don't get anything
-- for the 'SynType', because you've said positively that it should be an
-- Int, and so it shall be.
--
-- This is defined here to avoid defining it in TcExpr.hs-boot.
data SyntaxOpType
  = SynAny     -- ^ Any type
  | SynRho     -- ^ A rho type, deeply skolemised or instantiated as appropriate
  | SynList    -- ^ A list type. You get back the element type of the list
  | SynFun SyntaxOpType SyntaxOpType
               -- ^ A function.
  | SynType ExpType   -- ^ A known type.
infixr 0 `SynFun`

-- | Like 'SynType' but accepts a regular TcType
synKnownType :: TcType -> SyntaxOpType
synKnownType = SynType . mkCheckExpType

-- | Like 'mkFunTys' but for 'SyntaxOpType'
mkSynFunTys :: [SyntaxOpType] -> ExpType -> SyntaxOpType
mkSynFunTys arg_tys res_ty = foldr SynFun (SynType res_ty) arg_tys


Austin Seipp's avatar
Austin Seipp committed
404
{-
405 406 407 408 409 410 411 412
Note [TcRhoType]
~~~~~~~~~~~~~~~~
A TcRhoType has no foralls or contexts at the top, or to the right of an arrow
  YES    (forall a. a->a) -> Int
  NO     forall a. a ->  Int
  NO     Eq a => a -> a
  NO     Int -> forall a. a -> Int

413

Austin Seipp's avatar
Austin Seipp committed
414 415
************************************************************************
*                                                                      *
416
        TyVarDetails, MetaDetails, MetaInfo
Austin Seipp's avatar
Austin Seipp committed
417 418
*                                                                      *
************************************************************************
419

420 421
TyVarDetails gives extra info about type variables, used during type
checking.  It's attached to mutable type variables only.
422 423
It's knot-tied back to Var.hs.  There is no reason in principle
why Var.hs shouldn't actually have the definition, but it "belongs" here.
424

425 426 427 428
Note [Signature skolems]
~~~~~~~~~~~~~~~~~~~~~~~~
Consider this

429 430 431 432 433 434 435 436 437 438 439 440 441
  f :: forall a. [a] -> Int
  f (x::b : xs) = 3

Here 'b' is a lexically scoped type variable, but it turns out to be
the same as the skolem 'a'.  So we have a special kind of skolem
constant, SigTv, which can unify with other SigTvs. They are used
*only* for pattern type signatures.

Similarly consider
  data T (a:k1) = MkT (S a)
  data S (b:k2) = MkS (T b)
When doing kind inference on {S,T} we don't want *skolems* for k1,k2,
because they end up unifying; we want those SigTvs again.
442

443 444
Note [TyVars and TcTyVars during type checking]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
445 446 447
The Var type has constructors TyVar and TcTyVar.  They are used
as follows:

448
* TcTyVar: used /only/ during type checking.  Should never appear
449 450
  afterwards.  May contain a mutable field, in the MetaTv case.

451 452 453 454 455 456 457 458 459 460 461 462
* TyVar: is never seen by the constraint solver, except locally
  inside a type like (forall a. [a] ->[a]), where 'a' is a TyVar.
  We instantiate these with TcTyVars before exposing the type
  to the constraint solver.

I have swithered about the latter invariant, excluding TyVars from the
constraint solver.  It's not strictly essential, and indeed
(historically but still there) Var.tcTyVarDetails returns
vanillaSkolemTv for a TyVar.

But ultimately I want to seeparate Type from TcType, and in that case
we would need to enforce the separation.
Austin Seipp's avatar
Austin Seipp committed
463
-}
464

465
-- A TyVarDetails is inside a TyVar
466
-- See Note [TyVars and TcTyVars]
467
data TcTyVarDetails
468
  = SkolemTv      -- A skolem
469
       TcLevel    -- Level of the implication that binds it
470 471 472
       Bool       -- True <=> this skolem type variable can be overlapped
                  --          when looking up instances
                  -- See Note [Binding when looking up instances] in InstEnv
473

474 475 476 477
  | FlatSkol      -- A flatten-skolem.  It stands for the TcType, and zonking
       TcType     -- will replace it by that type.
                  -- See Note [The flattening story] in TcFlatten

478 479 480
  | RuntimeUnk    -- Stands for an as-yet-unknown type in the GHCi
                  -- interactive context

481 482
  | MetaTv { mtv_info  :: MetaInfo
           , mtv_ref   :: IORef MetaDetails
483
           , mtv_tclvl :: TcLevel }  -- See Note [TcLevel and untouchable type variables]
484

485 486
vanillaSkolemTv, superSkolemTv :: TcTyVarDetails
-- See Note [Binding when looking up instances] in InstEnv
487 488
vanillaSkolemTv = SkolemTv (pushTcLevel topTcLevel) False  -- Might be instantiated
superSkolemTv   = SkolemTv (pushTcLevel topTcLevel) True   -- Treat this as a completely distinct type
489

490
-----------------------------
491
data MetaDetails
492
  = Flexi  -- Flexi type variables unify to become Indirects
493 494
  | Indirect TcType

495
data MetaInfo
496
   = TauTv         -- This MetaTv is an ordinary unification variable
497
                   -- A TauTv is always filled in with a tau-type, which
thomasw's avatar
thomasw committed
498
                   -- never contains any ForAlls.
499

500 501 502 503 504 505
   | SigTv         -- A variant of TauTv, except that it should not be
                   -- unified with a type, only with a type variable
                   -- SigTvs are only distinguished to improve error messages
                   --      see Note [Signature skolems]
                   --      The MetaDetails, if filled in, will
                   --      always be another SigTv or a SkolemTv
506

507 508 509 510
   | FlatMetaTv    -- A flatten meta-tyvar
                   -- It is a meta-tyvar, but it is always untouchable, with level 0
                   -- See Note [The flattening story] in TcFlatten

511 512 513 514 515 516 517 518
instance Outputable MetaDetails where
  ppr Flexi         = text "Flexi"
  ppr (Indirect ty) = text "Indirect" <+> ppr ty

pprTcTyVarDetails :: TcTyVarDetails -> SDoc
-- For debugging
pprTcTyVarDetails (RuntimeUnk {})  = text "rt"
pprTcTyVarDetails (FlatSkol {})    = text "fsk"
519 520
pprTcTyVarDetails (SkolemTv lvl True)  = text "ssk" <> colon <> ppr lvl
pprTcTyVarDetails (SkolemTv lvl False) = text "sk"  <> colon <> ppr lvl
521 522 523 524 525 526 527 528 529 530 531 532 533 534 535
pprTcTyVarDetails (MetaTv { mtv_info = info, mtv_tclvl = tclvl })
  = pp_info <> colon <> ppr tclvl
  where
    pp_info = case info of
                TauTv      -> text "tau"
                SigTv      -> text "sig"
                FlatMetaTv -> text "fuv"


{- *********************************************************************
*                                                                      *
          UserTypeCtxt
*                                                                      *
********************************************************************* -}

536
-------------------------------------
537 538 539 540
-- UserTypeCtxt describes the origin of the polymorphic type
-- in the places where we need to an expression has that type

data UserTypeCtxt
541 542 543 544 545 546 547 548 549 550 551
  = FunSigCtxt      -- Function type signature, when checking the type
                    -- Also used for types in SPECIALISE pragmas
       Name              -- Name of the function
       Bool              -- True <=> report redundant constraints
                            -- This is usually True, but False for
                            --   * Record selectors (not important here)
                            --   * Class and instance methods.  Here
                            --     the code may legitimately be more
                            --     polymorphic than the signature
                            --     generated from the class
                            --     declaration
552

553 554
  | InfSigCtxt Name     -- Inferred type for function
  | ExprSigCtxt         -- Expression type signature
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
555
  | TypeAppCtxt         -- Visible type application
556 557
  | ConArgCtxt Name     -- Data constructor argument
  | TySynCtxt Name      -- RHS of a type synonym decl
558
  | PatSynCtxt Name     -- Type sig for a pattern synonym
559 560 561
  | PatSigCtxt          -- Type sig in pattern
                        --   eg  f (x::t) = ...
                        --   or  (x::t, y) = e
562 563
  | RuleSigCtxt Name    -- LHS of a RULE forall
                        --    RULE "foo" forall (x :: a -> a). f (Just x) = ...
564 565 566 567
  | ResSigCtxt          -- Result type sig
                        --      f x :: t = ....
  | ForSigCtxt Name     -- Foreign import or export signature
  | DefaultDeclCtxt     -- Types in a default declaration
dreixel's avatar
dreixel committed
568
  | InstDeclCtxt        -- An instance declaration
569 570
  | SpecInstCtxt        -- SPECIALISE instance pragma
  | ThBrackCtxt         -- Template Haskell type brackets [t| ... |]
571 572 573
  | GenSigCtxt          -- Higher-rank or impredicative situations
                        -- e.g. (f e) where f has a higher-rank type
                        -- We might want to elaborate this
574
  | GhciCtxt            -- GHCi command :kind <type>
575

576 577 578
  | ClassSCCtxt Name    -- Superclasses of a class
  | SigmaCtxt           -- Theta part of a normal for-all type
                        --      f :: <S> => a -> a
579
  | DataTyCtxt Name     -- The "stupid theta" part of a data decl
580
                        --      data <S> => T a = MkT a
dreixel's avatar
dreixel committed
581

Austin Seipp's avatar
Austin Seipp committed
582
{-
583 584 585
-- Notes re TySynCtxt
-- We allow type synonyms that aren't types; e.g.  type List = []
--
586
-- If the RHS mentions tyvars that aren't in scope, we'll
587
-- quantify over them:
588 589
--      e.g.    type T = a->a
-- will become  type T = forall a. a->a
590
--
591
-- With gla-exts that's right, but for H98 we should complain.
592
-}
593 594


595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624
pprUserTypeCtxt :: UserTypeCtxt -> SDoc
pprUserTypeCtxt (FunSigCtxt n _)  = text "the type signature for" <+> quotes (ppr n)
pprUserTypeCtxt (InfSigCtxt n)    = text "the inferred type for" <+> quotes (ppr n)
pprUserTypeCtxt (RuleSigCtxt n)   = text "a RULE for" <+> quotes (ppr n)
pprUserTypeCtxt ExprSigCtxt       = text "an expression type signature"
pprUserTypeCtxt TypeAppCtxt       = text "a type argument"
pprUserTypeCtxt (ConArgCtxt c)    = text "the type of the constructor" <+> quotes (ppr c)
pprUserTypeCtxt (TySynCtxt c)     = text "the RHS of the type synonym" <+> quotes (ppr c)
pprUserTypeCtxt ThBrackCtxt       = text "a Template Haskell quotation [t|...|]"
pprUserTypeCtxt PatSigCtxt        = text "a pattern type signature"
pprUserTypeCtxt ResSigCtxt        = text "a result type signature"
pprUserTypeCtxt (ForSigCtxt n)    = text "the foreign declaration for" <+> quotes (ppr n)
pprUserTypeCtxt DefaultDeclCtxt   = text "a type in a `default' declaration"
pprUserTypeCtxt InstDeclCtxt      = text "an instance declaration"
pprUserTypeCtxt SpecInstCtxt      = text "a SPECIALISE instance pragma"
pprUserTypeCtxt GenSigCtxt        = text "a type expected by the context"
pprUserTypeCtxt GhciCtxt          = text "a type in a GHCi command"
pprUserTypeCtxt (ClassSCCtxt c)   = text "the super-classes of class" <+> quotes (ppr c)
pprUserTypeCtxt SigmaCtxt         = text "the context of a polymorphic type"
pprUserTypeCtxt (DataTyCtxt tc)   = text "the context of the data type declaration for" <+> quotes (ppr tc)
pprUserTypeCtxt (PatSynCtxt n)    = text "the signature for pattern synonym" <+> quotes (ppr n)

isSigMaybe :: UserTypeCtxt -> Maybe Name
isSigMaybe (FunSigCtxt n _) = Just n
isSigMaybe (ConArgCtxt n)   = Just n
isSigMaybe (ForSigCtxt n)   = Just n
isSigMaybe (PatSynCtxt n)   = Just n
isSigMaybe _                = Nothing


625
{- *********************************************************************
Austin Seipp's avatar
Austin Seipp committed
626
*                                                                      *
627
                Untoucable type variables
Austin Seipp's avatar
Austin Seipp committed
628
*                                                                      *
629
********************************************************************* -}
630

631
newtype TcLevel = TcLevel Int deriving( Eq, Ord )
632
  -- See Note [TcLevel and untouchable type variables] for what this Int is
633
  -- See also Note [TcLevel assignment]
634

Austin Seipp's avatar
Austin Seipp committed
635
{-
636 637
Note [TcLevel and untouchable type variables]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
638
* Each unification variable (MetaTv)
639
  and each Implication
640
  has a level number (of type TcLevel)
641

642 643 644
* INVARIANTS.  In a tree of Implications,

    (ImplicInv) The level number of an Implication is
645 646
                STRICTLY GREATER THAN that of its parent

647 648
    (MetaTvInv) The level number of a unification variable is
                LESS THAN OR EQUAL TO that of its parent
649 650 651 652 653
                implication

* A unification variable is *touchable* if its level number
  is EQUAL TO that of its immediate parent implication.

654 655 656
* INVARIANT
    (GivenInv)  The free variables of the ic_given of an
                implication are all untouchable; ie their level
657
                numbers are LESS THAN the ic_tclvl of the implication
658

659 660 661
Note [Skolem escape prevention]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We only unify touchable unification variables.  Because of
662 663
(MetaTvInv), there can be no occurrences of the variable further out,
so the unification can't cause the skolems to escape. Example:
664 665 666 667 668 669 670 671 672 673 674 675
     data T = forall a. MkT a (a->Int)
     f x (MkT v f) = length [v,x]
We decide (x::alpha), and generate an implication like
      [1]forall a. (a ~ alpha[0])
But we must not unify alpha:=a, because the skolem would escape.

For the cases where we DO want to unify, we rely on floating the
equality.   Example (with same T)
     g x (MkT v f) = x && True
We decide (x::alpha), and generate an implication like
      [1]forall a. (Bool ~ alpha[0])
We do NOT unify directly, bur rather float out (if the constraint
Krzysztof Gogolewski's avatar
Typos  
Krzysztof Gogolewski committed
676
does not mention 'a') to get
677 678 679 680 681
      (Bool ~ alpha[0]) /\ [1]forall a.()
and NOW we can unify alpha.

The same idea of only unifying touchables solves another problem.
Suppose we had
682 683
   (F Int ~ uf[0])  /\  [1](forall a. C a => F Int ~ beta[1])
In this example, beta is touchable inside the implication. The
684
first solveSimpleWanteds step leaves 'uf' un-unified. Then we move inside
685
the implication where a new constraint
686 687 688
       uf  ~  beta
emerges. If we (wrongly) spontaneously solved it to get uf := beta,
the whole implication disappears but when we pop out again we are left with
689
(F Int ~ uf) which will be unified by our final zonking stage and
690
uf will get unified *once more* to (F Int).
691 692 693 694 695

Note [TcLevel assignment]
~~~~~~~~~~~~~~~~~~~~~~~~~
We arrange the TcLevels like this

696
   0   Level for flatten meta-vars
697
   1   Top level
698 699
   2   First-level implication constraints
   3   Second-level implication constraints
700 701
   ...etc...

702
The flatten meta-vars are all at level 0, just to make them untouchable.
Austin Seipp's avatar
Austin Seipp committed
703
-}
704

705 706 707
maxTcLevel :: TcLevel -> TcLevel -> TcLevel
maxTcLevel (TcLevel a) (TcLevel b) = TcLevel (a `max` b)

708
fmvTcLevel :: TcLevel -> TcLevel
709
-- See Note [TcLevel assignment]
710
fmvTcLevel _ = TcLevel 0
711

712
topTcLevel :: TcLevel
713
-- See Note [TcLevel assignment]
714
topTcLevel = TcLevel 1   -- 1 = outermost level
715

716 717 718 719
isTopTcLevel :: TcLevel -> Bool
isTopTcLevel (TcLevel 1) = True
isTopTcLevel _           = False

720
pushTcLevel :: TcLevel -> TcLevel
721
-- See Note [TcLevel assignment]
722
pushTcLevel (TcLevel us) = TcLevel (us + 1)
723

724 725 726
strictlyDeeperThan :: TcLevel -> TcLevel -> Bool
strictlyDeeperThan (TcLevel tv_tclvl) (TcLevel ctxt_tclvl)
  = tv_tclvl > ctxt_tclvl
727

728 729 730
sameDepthAs :: TcLevel -> TcLevel -> Bool
sameDepthAs (TcLevel ctxt_tclvl) (TcLevel tv_tclvl)
  = ctxt_tclvl == tv_tclvl   -- NB: invariant ctxt_tclvl >= tv_tclvl
731 732
                             --     So <= would be equivalent

733 734 735 736
checkTcLevelInvariant :: TcLevel -> TcLevel -> Bool
-- Checks (MetaTvInv) from Note [TcLevel and untouchable type variables]
checkTcLevelInvariant (TcLevel ctxt_tclvl) (TcLevel tv_tclvl)
  = ctxt_tclvl >= tv_tclvl
737

738 739
tcTyVarLevel :: TcTyVar -> TcLevel
tcTyVarLevel tv
Simon Peyton Jones's avatar
Simon Peyton Jones committed
740
  = ASSERT2( tcIsTcTyVar tv, ppr tv )
741 742 743 744 745 746 747 748 749 750 751 752 753 754 755
    case tcTyVarDetails tv of
          MetaTv { mtv_tclvl = tv_lvl } -> tv_lvl
          SkolemTv tv_lvl _             -> tv_lvl
          FlatSkol ty                   -> tcTypeLevel ty
          RuntimeUnk                    -> topTcLevel

tcTypeLevel :: TcType -> TcLevel
-- Max level of any free var of the type
tcTypeLevel ty
  = foldDVarSet add topTcLevel (tyCoVarsOfTypeDSet ty)
  where
    add v lvl
      | isTcTyVar v = lvl `maxTcLevel` tcTyVarLevel v
      | otherwise   = lvl

756 757
instance Outputable TcLevel where
  ppr (TcLevel us) = ppr us
758

759
{- *********************************************************************
Austin Seipp's avatar
Austin Seipp committed
760
*                                                                      *
761
    Finding type family instances
762
*                                                                      *
Austin Seipp's avatar
Austin Seipp committed
763 764
************************************************************************
-}
765

Simon Peyton Jones's avatar
Simon Peyton Jones committed
766
-- | Finds outermost type-family applications occuring in a type,
767 768 769 770 771 772 773 774 775 776 777
-- after expanding synonyms.  In the list (F, tys) that is returned
-- we guarantee that tys matches F's arity.  For example, given
--    type family F a :: * -> *    (arity 1)
-- calling tcTyFamInsts on (Maybe (F Int Bool) will return
--     (F, [Int]), not (F, [Int,Bool])
--
-- This is important for its use in deciding termination of type
-- instances (see Trac #11581).  E.g.
--    type instance G [Int] = ...(F Int <big type>)...
-- we don't need to take <big type> into account when asking if
-- the calls on the RHS are smaller than the LHS
778
tcTyFamInsts :: Type -> [(TyCon, [Type])]
779
tcTyFamInsts ty
780
  | Just exp_ty <- coreView ty  = tcTyFamInsts exp_ty
781
tcTyFamInsts (TyVarTy _)        = []
782
tcTyFamInsts (TyConApp tc tys)
783
  | isTypeFamilyTyCon tc        = [(tc, take (tyConArity tc) tys)]
784
  | otherwise                   = concat (map tcTyFamInsts tys)
785
tcTyFamInsts (LitTy {})         = []
786
tcTyFamInsts (ForAllTy bndr ty) = tcTyFamInsts (binderKind bndr)
787
                                  ++ tcTyFamInsts ty
Simon Peyton Jones's avatar
Simon Peyton Jones committed
788
tcTyFamInsts (FunTy ty1 ty2)    = tcTyFamInsts ty1 ++ tcTyFamInsts ty2
789
tcTyFamInsts (AppTy ty1 ty2)    = tcTyFamInsts ty1 ++ tcTyFamInsts ty2
790 791 792
tcTyFamInsts (CastTy ty _)      = tcTyFamInsts ty
tcTyFamInsts (CoercionTy _)     = []  -- don't count tyfams in coercions,
                                      -- as they never get normalized, anyway
793

Austin Seipp's avatar
Austin Seipp committed
794 795
{-
************************************************************************
796
*                                                                      *
797
          The "exact" free variables of a type
798
*                                                                      *
Austin Seipp's avatar
Austin Seipp committed
799
************************************************************************
800 801 802 803 804

Note [Silly type synonym]
~~~~~~~~~~~~~~~~~~~~~~~~~
Consider
  type T a = Int
805
What are the free tyvars of (T x)?  Empty, of course!
806 807 808 809 810 811 812 813 814 815
Here's the example that Ralf Laemmel showed me:
  foo :: (forall a. C u a -> C u a) -> u
  mappend :: Monoid u => u -> u -> u

  bar :: Monoid u => u
  bar = foo (\t -> t `mappend` t)
We have to generalise at the arg to f, and we don't
want to capture the constraint (Monad (C u a)) because
it appears to mention a.  Pretty silly, but it was useful to him.

816
exactTyCoVarsOfType is used by the type checker to figure out exactly
817 818 819 820 821 822
which type variables are mentioned in a type.  It's also used in the
smart-app checking code --- see TcExpr.tcIdApp

On the other hand, consider a *top-level* definition
  f = (\x -> x) :: T a -> T a
If we don't abstract over 'a' it'll get fixed to GHC.Prim.Any, and then
823
if we have an application like (f "x") we get a confusing error message
824
involving Any.  So the conclusion is this: when generalising
825 826
  - at top level use tyCoVarsOfType
  - in nested bindings use exactTyCoVarsOfType
827
See Trac #1813 for example.
Austin Seipp's avatar
Austin Seipp committed
828
-}
829

830
exactTyCoVarsOfType :: Type -> TyCoVarSet
831 832
-- Find the free type variables (of any kind)
-- but *expand* type synonyms.  See Note [Silly type synonym] above.
833
exactTyCoVarsOfType ty
834 835
  = go ty
  where
836
    go ty | Just ty' <- coreView ty = go ty'  -- This is the key line
837
    go (TyVarTy tv)         = unitVarSet tv `unionVarSet` go (tyVarKind tv)
838
    go (TyConApp _ tys)     = exactTyCoVarsOfTypes tys
839
    go (LitTy {})           = emptyVarSet
840
    go (AppTy fun arg)      = go fun `unionVarSet` go arg
Simon Peyton Jones's avatar
Simon Peyton Jones committed
841
    go (FunTy arg res)      = go arg `unionVarSet` go res
842
    go (ForAllTy bndr ty)   = delBinderVar (go ty) bndr `unionVarSet` go (binderKind bndr)
843 844 845 846 847 848 849 850 851 852 853 854 855 856 857 858 859 860 861 862 863 864 865 866 867 868 869 870 871 872 873
    go (CastTy ty co)       = go ty `unionVarSet` goCo co
    go (CoercionTy co)      = goCo co

    goCo (Refl _ ty)        = go ty
    goCo (TyConAppCo _ _ args)= goCos args
    goCo (AppCo co arg)     = goCo co `unionVarSet` goCo arg
    goCo (ForAllCo tv k_co co)
      = goCo co `delVarSet` tv `unionVarSet` goCo k_co
    goCo (CoVarCo v)         = unitVarSet v `unionVarSet` go (varType v)
    goCo (AxiomInstCo _ _ args) = goCos args
    goCo (UnivCo p _ t1 t2)  = goProv p `unionVarSet` go t1 `unionVarSet` go t2
    goCo (SymCo co)          = goCo co
    goCo (TransCo co1 co2)   = goCo co1 `unionVarSet` goCo co2
    goCo (NthCo _ co)        = goCo co
    goCo (LRCo _ co)         = goCo co
    goCo (InstCo co arg)     = goCo co `unionVarSet` goCo arg
    goCo (CoherenceCo c1 c2) = goCo c1 `unionVarSet` goCo c2
    goCo (KindCo co)         = goCo co
    goCo (SubCo co)          = goCo co
    goCo (AxiomRuleCo _ c)   = goCos c

    goCos cos = foldr (unionVarSet . goCo) emptyVarSet cos

    goProv UnsafeCoerceProv     = emptyVarSet
    goProv (PhantomProv kco)    = goCo kco
    goProv (ProofIrrelProv kco) = goCo kco
    goProv (PluginProv _)       = emptyVarSet
    goProv (HoleProv _)         = emptyVarSet

exactTyCoVarsOfTypes :: [Type] -> TyVarSet
exactTyCoVarsOfTypes tys = mapUnionVarSet exactTyCoVarsOfType tys
874

875 876 877 878
rewritableTyVarsOfTypes :: [TcType] -> TcTyVarSet
rewritableTyVarsOfTypes tys = mapUnionVarSet rewritableTyVarsOfType tys

rewritableTyVarsOfType :: TcType -> TcTyVarSet
Simon Peyton Jones's avatar
Simon Peyton Jones committed
879 880 881
-- Used during kick-out from the inert set
-- Ignores coercions and casts, because rewriting those does
-- not help solving, and it's more efficient to ignore them
882 883 884 885 886 887 888 889 890 891 892 893 894
rewritableTyVarsOfType ty
  = go ty
  where
    go (TyVarTy tv)     = unitVarSet tv
    go (LitTy {})</