TcType.hs 103 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, ScopedTypeVariables, MultiWayIf, FlexibleContexts #-}
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,
61
  tcSplitForAllTys, tcSplitPiTys, tcSplitPiTy_maybe, tcSplitForAllTyVarBndrs,
62
  tcSplitPhiTy, tcSplitPredFunTy_maybe,
Richard Eisenberg's avatar
Richard Eisenberg committed
63 64
  tcSplitFunTy_maybe, tcSplitFunTys, tcFunArgTy, tcFunResultTy, tcFunResultTyN,
  tcSplitFunTysN,
Ben Gamari's avatar
Ben Gamari committed
65 66 67
  tcSplitTyConApp, tcSplitTyConApp_maybe,
  tcRepSplitTyConApp_maybe, tcRepSplitTyConApp_maybe',
  tcTyConAppTyCon, tcTyConAppTyCon_maybe, tcTyConAppArgs,
68
  tcSplitAppTy_maybe, tcSplitAppTy, tcSplitAppTys, tcRepSplitAppTy_maybe,
69
  tcRepGetNumAppTys,
70
  tcGetCastedTyVar_maybe, tcGetTyVar_maybe, tcGetTyVar, nextRole,
71
  tcSplitSigmaTy, tcSplitNestedSigmaTys, tcDeepSplitSigmaTy_maybe,
72 73

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

86 87
  ---------------------------------
  -- Misc type manipulators
88 89

  deNoteType,
Simon Peyton Jones's avatar
Simon Peyton Jones committed
90
  orphNamesOfType, orphNamesOfCo,
91
  orphNamesOfTypes, orphNamesOfCoCon,
92
  getDFunTyKey,
93
  evVarPred_maybe, evVarPred,
94 95

  ---------------------------------
96
  -- Predicate types
97
  mkMinimalBySCs, transSuperClasses,
98
  pickQuantifiablePreds, pickCapturedPreds,
99 100
  immSuperClasses,
  isImprovementPred,
101

102
  -- * Finding type instances
103
  tcTyFamInsts, isTyFamFree,
104 105

  -- * Finding "exact" (non-dead) type variables
106
  exactTyCoVarsOfType, exactTyCoVarsOfTypes,
107
  candidateQTyVarsOfType, candidateQTyVarsOfTypes, CandidatesQTvs(..),
108
  anyRewritableTyVar,
109 110 111

  -- * Extracting bound variables
  allBoundVariables, allBoundVariabless,
112

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

127
  --------------------------------
128 129
  -- Rexported from Kind
  Kind, typeKind,
130
  liftedTypeKind,
131 132
  constraintKind,
  isLiftedTypeKind, isUnliftedTypeKind, classifiesTypeWithValues,
133

134 135
  --------------------------------
  -- Rexported from Type
136
  Type, PredType, ThetaType, TyBinder, ArgFlag(..),
137

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

144
  isClassPred, isEqPred, isNomEqPred, isIPPred,
145
  mkClassPred,
146
  isDictLikeTy,
147
  tcSplitDFunTy, tcSplitDFunHead, tcSplitMethodTy,
Richard Eisenberg's avatar
Richard Eisenberg committed
148
  isRuntimeRepVar, isKindLevPoly,
149
  isVisibleBinder, isInvisibleBinder,
150

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

168
  isUnliftedType,       -- Source types are always lifted
169 170
  isUnboxedTupleType,   -- Ditto
  isPrimitiveType,
171

Ben Gamari's avatar
Ben Gamari committed
172
  tcView, coreView,
173 174

  tyCoVarsOfType, tyCoVarsOfTypes, closeOverKinds,
niteria's avatar
niteria committed
175
  tyCoFVsOfType, tyCoFVsOfTypes,
176 177
  tyCoVarsOfTypeDSet, tyCoVarsOfTypesDSet, closeOverKindsDSet,
  tyCoVarsOfTypeList, tyCoVarsOfTypesList,
Richard Eisenberg's avatar
Richard Eisenberg committed
178
  noFreeVarsOfType,
179

180 181 182 183 184
  --------------------------------
  -- Transforming Types to TcTypes
  toTcType,    -- :: Type -> TcType
  toTcTypeBag, -- :: Bag EvVar -> Bag EvVar

185
  pprKind, pprParendKind, pprSigmaType,
186
  pprType, pprParendType, pprTypeApp, pprTyThingCategory, tyThingCategory,
187
  pprTheta, pprParendTheta, pprThetaArrowTy, pprClassPred,
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
188
  pprTvBndr, pprTvBndrs,
189

190 191 192 193 194
  TypeSize, sizeType, sizeTypes, toposortTyVars,

  ---------------------------------
  -- argument visibility
  tcTyConVisibilities, isNextTyConArgVisible, isNextArgVisible
195

196
  ) where
197

198
#include "HsVersions.h"
199

200
-- friends:
201 202
import GhcPrelude

203
import Kind
204
import TyCoRep
205 206 207
import Class
import Var
import ForeignCall
208
import VarSet
209
import Coercion
210
import Type
Richard Eisenberg's avatar
Richard Eisenberg committed
211
import RepType
212
import TyCon
213 214

-- others:
215
import DynFlags
Simon Peyton Jones's avatar
Simon Peyton Jones committed
216
import CoreFVs
217 218 219
import Name -- hiding (varName)
            -- We use this to make dictionaries for type literals.
            -- Perhaps there's a better way to do this?
220
import NameSet
221 222
import VarEnv
import PrelNames
223 224
import TysWiredIn( coercibleClass, unitTyCon, unitTyConKey
                 , listTyCon, constraintKind )
225 226
import BasicTypes
import Util
227
import Bag
228
import Maybes
229
import ListSetOps ( getNth )
230
import Outputable
231
import FastString
232
import ErrUtils( Validity(..), MsgDoc, isValid )
233
import FV
234
import qualified GHC.LanguageExtensions as LangExt
Simon Marlow's avatar
Simon Marlow committed
235 236

import Data.IORef
237
import Data.Functor.Identity
238
import qualified Data.Semigroup as Semi
239

Austin Seipp's avatar
Austin Seipp committed
240 241 242
{-
************************************************************************
*                                                                      *
243
              Types
Austin Seipp's avatar
Austin Seipp committed
244 245
*                                                                      *
************************************************************************
246

247
The type checker divides the generic Type world into the
248 249
following more structured beasts:

250
sigma ::= forall tyvars. phi
251 252 253 254
        -- A sigma type is a qualified type
        --
        -- Note that even if 'tyvars' is empty, theta
        -- may not be: e.g.   (?x::Int) => Int
255

256 257 258 259
        -- 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
260

261 262 263
phi :: theta => rho

rho ::= sigma -> rho
264 265 266 267 268 269 270 271 272 273 274
     |  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
275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294

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
295
    may see free occurrences of 'k'.
Simon Peyton Jones's avatar
Simon Peyton Jones committed
296

297 298 299 300
    See calls to tcExtendTyVarEnv for other places that ordinary
    TyVars are bought into scope, and hence may show up in the types
    and inds generated by TcHsType.

Simon Peyton Jones's avatar
Simon Peyton Jones committed
301 302 303 304 305 306 307 308 309 310 311 312 313 314
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.
315 316 317 318 319 320 321 322 323 324 325 326

Note [Coercion variables in free variable lists]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
There are several places in the GHC codebase where functions like
tyCoVarsOfType, tyCoVarsOfCt, et al. are used to compute the free type
variables of a type. The "Co" part of these functions' names shouldn't be
dismissed, as it is entirely possible that they will include coercion variables
in addition to type variables! As a result, there are some places in TcType
where we must take care to check that a variable is a _type_ variable (using
isTyVar) before calling tcTyVarDetails--a partial function that is not defined
for coercion variables--on the variable. Failing to do so led to
GHC Trac #12785.
Austin Seipp's avatar
Austin Seipp committed
327
-}
328

Simon Peyton Jones's avatar
Simon Peyton Jones committed
329
-- See Note [TcTyVars in the typechecker]
330
type TcTyVar = TyVar    -- Used only during type inference
331
type TcCoVar = CoVar    -- Used only during type inference
332
type TcType = Type      -- A TcType can have mutable type variables
333
type TcTyCoVar = Var    -- Either a TcTyVar or a CoVar
334 335 336 337
        -- 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
338 339 340

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

342
-- These types do not have boxy type variables in them
343 344
type TcPredType     = PredType
type TcThetaType    = ThetaType
345
type TcSigmaType    = TcType
346
type TcRhoType      = TcType  -- Note [TcRhoType]
347
type TcTauType      = TcType
348
type TcKind         = Kind
349
type TcTyVarSet     = TyVarSet
350
type TcTyCoVarSet   = TyCoVarSet
351
type TcDTyVarSet    = DTyVarSet
352
type TcDTyCoVarSet  = DTyCoVarSet
353

354 355 356 357 358 359 360

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

361 362 363
-- | An expected type to check against during type-checking.
-- See Note [ExpType] in TcMType, where you'll also find manipulators.
data ExpType = Check TcType
364 365 366 367 368 369 370
             | 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
371
                            -- False <=> do not instantiate before returning
372 373
                            --           i.e. return a SigmaType
       , ir_ref  :: IORef (Maybe TcType) }
374 375
         -- The type that fills in this hole should be a Type,
         -- that is, its kind should be (TYPE rr) for some rr
376 377 378 379 380

type ExpSigmaType = ExpType
type ExpRhoType   = ExpType

instance Outputable ExpType where
381 382 383 384 385
  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
386
          , ir_inst = inst })
387
    = text "Infer" <> braces (ppr u <> comma <> ppr lvl <+> ppr inst)
388 389 390 391 392

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

393 394 395 396 397 398 399

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

400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431
-- | 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
432
{-
433 434 435 436 437 438 439 440
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

441

Austin Seipp's avatar
Austin Seipp committed
442 443
************************************************************************
*                                                                      *
444
        TyVarDetails, MetaDetails, MetaInfo
Austin Seipp's avatar
Austin Seipp committed
445 446
*                                                                      *
************************************************************************
447

448 449
TyVarDetails gives extra info about type variables, used during type
checking.  It's attached to mutable type variables only.
450 451
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.
452

453 454
Note [Signature skolems]
~~~~~~~~~~~~~~~~~~~~~~~~
455 456 457 458 459 460 461 462 463
A SigTv is a specialised variant of TauTv, with the following invarints:

    * A SigTv can be unified only with a TyVar,
      not with any other type

    * Its MetaDetails, if filled in, will always be another SigTv
      or a SkolemTv

SigTvs are only distinguished to improve error messages.
464 465
Consider this

466 467 468 469
  f :: forall a. [a] -> Int
  f (x::b : xs) = 3

Here 'b' is a lexically scoped type variable, but it turns out to be
470 471
the same as the skolem 'a'.  So we make them both SigTvs, which can unify
with each other.
472 473 474 475 476 477

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.
478

479 480
SigTvs are used *only* for pattern type signatures.

481 482
Note [TyVars and TcTyVars during type checking]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
483 484 485
The Var type has constructors TyVar and TcTyVar.  They are used
as follows:

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

489 490 491 492 493 494 495 496 497 498 499 500
* 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
501
-}
502

503
-- A TyVarDetails is inside a TyVar
504
-- See Note [TyVars and TcTyVars]
505
data TcTyVarDetails
506
  = SkolemTv      -- A skolem
507
       TcLevel    -- Level of the implication that binds it
508 509 510
       Bool       -- True <=> this skolem type variable can be overlapped
                  --          when looking up instances
                  -- See Note [Binding when looking up instances] in InstEnv
511

512 513 514
  | RuntimeUnk    -- Stands for an as-yet-unknown type in the GHCi
                  -- interactive context

515 516
  | MetaTv { mtv_info  :: MetaInfo
           , mtv_ref   :: IORef MetaDetails
517
           , mtv_tclvl :: TcLevel }  -- See Note [TcLevel and untouchable type variables]
518

519 520
vanillaSkolemTv, superSkolemTv :: TcTyVarDetails
-- See Note [Binding when looking up instances] in InstEnv
521 522
vanillaSkolemTv = SkolemTv (pushTcLevel topTcLevel) False  -- Might be instantiated
superSkolemTv   = SkolemTv (pushTcLevel topTcLevel) True   -- Treat this as a completely distinct type
523

524
-----------------------------
525
data MetaDetails
526
  = Flexi  -- Flexi type variables unify to become Indirects
527 528
  | Indirect TcType

529
data MetaInfo
530
   = TauTv         -- This MetaTv is an ordinary unification variable
531
                   -- A TauTv is always filled in with a tau-type, which
thomasw's avatar
thomasw committed
532
                   -- never contains any ForAlls.
533

534
   | SigTv         -- A variant of TauTv, except that it should not be
535
                   --   unified with a type, only with a type variable
536
                   -- See Note [Signature skolems]
537

538 539 540 541
   | 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

542 543 544 545 546 547
   | FlatSkolTv    -- A flatten skolem tyvar
                   -- Just like FlatMetaTv, but is comletely "owned" by
                   --   its Given CFunEqCan.
                   -- It is filled in /only/ by unflattenGivens
                   -- See Note [The flattening story] in TcFlatten

548 549 550 551 552 553
instance Outputable MetaDetails where
  ppr Flexi         = text "Flexi"
  ppr (Indirect ty) = text "Indirect" <+> ppr ty

pprTcTyVarDetails :: TcTyVarDetails -> SDoc
-- For debugging
554
pprTcTyVarDetails (RuntimeUnk {})      = text "rt"
555 556
pprTcTyVarDetails (SkolemTv lvl True)  = text "ssk" <> colon <> ppr lvl
pprTcTyVarDetails (SkolemTv lvl False) = text "sk"  <> colon <> ppr lvl
557 558 559 560 561 562
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"
563 564
                FlatMetaTv -> text "fmv"
                FlatSkolTv -> text "fsk"
565 566 567 568 569 570 571 572


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

573
-------------------------------------
574 575 576 577
-- UserTypeCtxt describes the origin of the polymorphic type
-- in the places where we need to an expression has that type

data UserTypeCtxt
578 579 580 581 582 583 584 585 586 587 588
  = 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
589

590 591
  | InfSigCtxt Name     -- Inferred type for function
  | ExprSigCtxt         -- Expression type signature
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
592
  | TypeAppCtxt         -- Visible type application
593 594
  | ConArgCtxt Name     -- Data constructor argument
  | TySynCtxt Name      -- RHS of a type synonym decl
595
  | PatSynCtxt Name     -- Type sig for a pattern synonym
596 597 598
  | PatSigCtxt          -- Type sig in pattern
                        --   eg  f (x::t) = ...
                        --   or  (x::t, y) = e
599 600
  | RuleSigCtxt Name    -- LHS of a RULE forall
                        --    RULE "foo" forall (x :: a -> a). f (Just x) = ...
601 602 603 604
  | 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
605
  | InstDeclCtxt        -- An instance declaration
606 607
  | SpecInstCtxt        -- SPECIALISE instance pragma
  | ThBrackCtxt         -- Template Haskell type brackets [t| ... |]
608 609 610
  | GenSigCtxt          -- Higher-rank or impredicative situations
                        -- e.g. (f e) where f has a higher-rank type
                        -- We might want to elaborate this
611
  | GhciCtxt            -- GHCi command :kind <type>
612

613 614 615
  | ClassSCCtxt Name    -- Superclasses of a class
  | SigmaCtxt           -- Theta part of a normal for-all type
                        --      f :: <S> => a -> a
616
  | DataTyCtxt Name     -- The "stupid theta" part of a data decl
617
                        --      data <S> => T a = MkT a
dreixel's avatar
dreixel committed
618

Austin Seipp's avatar
Austin Seipp committed
619
{-
620 621 622
-- Notes re TySynCtxt
-- We allow type synonyms that aren't types; e.g.  type List = []
--
623
-- If the RHS mentions tyvars that aren't in scope, we'll
624
-- quantify over them:
625 626
--      e.g.    type T = a->a
-- will become  type T = forall a. a->a
627
--
628
-- With gla-exts that's right, but for H98 we should complain.
629
-}
630 631


632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661
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


662
{- *********************************************************************
Austin Seipp's avatar
Austin Seipp committed
663
*                                                                      *
664
                Untoucable type variables
Austin Seipp's avatar
Austin Seipp committed
665
*                                                                      *
666
********************************************************************* -}
667

668
newtype TcLevel = TcLevel Int deriving( Eq, Ord )
669
  -- See Note [TcLevel and untouchable type variables] for what this Int is
670
  -- See also Note [TcLevel assignment]
671

Austin Seipp's avatar
Austin Seipp committed
672
{-
673 674
Note [TcLevel and untouchable type variables]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
675
* Each unification variable (MetaTv)
676
  and each Implication
677
  has a level number (of type TcLevel)
678

679 680 681
* INVARIANTS.  In a tree of Implications,

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

684 685
    (MetaTvInv) The level number of a unification variable is
                LESS THAN OR EQUAL TO that of its parent
686 687 688 689 690
                implication

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

691 692 693
* INVARIANT
    (GivenInv)  The free variables of the ic_given of an
                implication are all untouchable; ie their level
694
                numbers are LESS THAN the ic_tclvl of the implication
695

696 697 698
Note [Skolem escape prevention]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We only unify touchable unification variables.  Because of
699 700
(MetaTvInv), there can be no occurrences of the variable further out,
so the unification can't cause the skolems to escape. Example:
701 702 703 704 705 706 707 708 709 710 711 712
     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
713
does not mention 'a') to get
714 715 716 717 718
      (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
719 720
   (F Int ~ uf[0])  /\  [1](forall a. C a => F Int ~ beta[1])
In this example, beta is touchable inside the implication. The
721
first solveSimpleWanteds step leaves 'uf' un-unified. Then we move inside
722
the implication where a new constraint
723 724 725
       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
726
(F Int ~ uf) which will be unified by our final zonking stage and
727
uf will get unified *once more* to (F Int).
728 729 730 731 732

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

733
   0   Level for all flatten meta-vars
734
   1   Top level
735 736
   2   First-level implication constraints
   3   Second-level implication constraints
737 738
   ...etc...

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

742 743 744
maxTcLevel :: TcLevel -> TcLevel -> TcLevel
maxTcLevel (TcLevel a) (TcLevel b) = TcLevel (a `max` b)

745
fmvTcLevel :: TcLevel
746
-- See Note [TcLevel assignment]
747
fmvTcLevel = TcLevel 0
748

749
topTcLevel :: TcLevel
750
-- See Note [TcLevel assignment]
751
topTcLevel = TcLevel 1   -- 1 = outermost level
752

753 754 755 756
isTopTcLevel :: TcLevel -> Bool
isTopTcLevel (TcLevel 1) = True
isTopTcLevel _           = False

757
pushTcLevel :: TcLevel -> TcLevel
758
-- See Note [TcLevel assignment]
759
pushTcLevel (TcLevel us) = TcLevel (us + 1)
760

761 762 763
strictlyDeeperThan :: TcLevel -> TcLevel -> Bool
strictlyDeeperThan (TcLevel tv_tclvl) (TcLevel ctxt_tclvl)
  = tv_tclvl > ctxt_tclvl
764

765 766 767
sameDepthAs :: TcLevel -> TcLevel -> Bool
sameDepthAs (TcLevel ctxt_tclvl) (TcLevel tv_tclvl)
  = ctxt_tclvl == tv_tclvl   -- NB: invariant ctxt_tclvl >= tv_tclvl
768 769
                             --     So <= would be equivalent

770 771 772 773
checkTcLevelInvariant :: TcLevel -> TcLevel -> Bool
-- Checks (MetaTvInv) from Note [TcLevel and untouchable type variables]
checkTcLevelInvariant (TcLevel ctxt_tclvl) (TcLevel tv_tclvl)
  = ctxt_tclvl >= tv_tclvl
774

775 776
tcTyVarLevel :: TcTyVar -> TcLevel
tcTyVarLevel tv
Simon Peyton Jones's avatar
Simon Peyton Jones committed
777
  = ASSERT2( tcIsTcTyVar tv, ppr tv )
778 779 780 781 782 783 784 785 786 787 788 789 790 791
    case tcTyVarDetails tv of
          MetaTv { mtv_tclvl = tv_lvl } -> tv_lvl
          SkolemTv tv_lvl _             -> tv_lvl
          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

792 793
instance Outputable TcLevel where
  ppr (TcLevel us) = ppr us
794

795
{- *********************************************************************
Austin Seipp's avatar
Austin Seipp committed
796
*                                                                      *
797
    Finding type family instances
798
*                                                                      *
Austin Seipp's avatar
Austin Seipp committed
799 800
************************************************************************
-}
801

Simon Peyton Jones's avatar
Simon Peyton Jones committed
802
-- | Finds outermost type-family applications occuring in a type,
803 804 805 806 807 808 809 810 811 812 813
-- 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
814
tcTyFamInsts :: Type -> [(TyCon, [Type])]
815
tcTyFamInsts ty
Ben Gamari's avatar
Ben Gamari committed
816
  | Just exp_ty <- tcView ty    = tcTyFamInsts exp_ty
817
tcTyFamInsts (TyVarTy _)        = []
818
tcTyFamInsts (TyConApp tc tys)
819
  | isTypeFamilyTyCon tc        = [(tc, take (tyConArity tc) tys)]
820
  | otherwise                   = concat (map tcTyFamInsts tys)
821
tcTyFamInsts (LitTy {})         = []
822
tcTyFamInsts (ForAllTy bndr ty) = tcTyFamInsts (binderKind bndr)
823
                                  ++ tcTyFamInsts ty
Simon Peyton Jones's avatar
Simon Peyton Jones committed
824
tcTyFamInsts (FunTy ty1 ty2)    = tcTyFamInsts ty1 ++ tcTyFamInsts ty2
825
tcTyFamInsts (AppTy ty1 ty2)    = tcTyFamInsts ty1 ++ tcTyFamInsts ty2
826 827 828
tcTyFamInsts (CastTy ty _)      = tcTyFamInsts ty
tcTyFamInsts (CoercionTy _)     = []  -- don't count tyfams in coercions,
                                      -- as they never get normalized, anyway
829

830 831 832 833
isTyFamFree :: Type -> Bool
-- ^ Check that a type does not contain any type family applications.
isTyFamFree = null . tcTyFamInsts

Austin Seipp's avatar
Austin Seipp committed
834 835
{-
************************************************************************
836
*                                                                      *
837
          The "exact" free variables of a type
838
*                                                                      *
Austin Seipp's avatar
Austin Seipp committed
839
************************************************************************
840 841 842 843 844

Note [Silly type synonym]
~~~~~~~~~~~~~~~~~~~~~~~~~
Consider
  type T a = Int
845
What are the free tyvars of (T x)?  Empty, of course!
846 847 848 849 850 851 852 853 854 855
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.

856
exactTyCoVarsOfType is used by the type checker to figure out exactly
857 858 859 860 861 862
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
863
if we have an application like (f "x") we get a confusing error message
864
involving Any.  So the conclusion is this: when generalising
865 866
  - at top level use tyCoVarsOfType
  - in nested bindings use exactTyCoVarsOfType
867
See Trac #1813 for example.
Austin Seipp's avatar
Austin Seipp committed
868
-}
869

870
exactTyCoVarsOfType :: Type -> TyCoVarSet