TcType.hs 88.9 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 25
  TcTyVar, TcTyVarSet, TcDTyVarSet, TcTyCoVarSet, TcDTyCoVarSet,
  TcKind, TcCoVar, TcTyCoVar, TcTyBinder,
26

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

  SyntaxOpType(..), synKnownType, mkSynFunTys,

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

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

  --------------------------------
51
  -- Builders
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
52
  mkPhiTy, mkInvSigmaTy, 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 62
  tcSplitForAllTys, tcSplitPiTys, tcSplitNamedPiTys,
  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
73 74
  eqType, eqTypes, cmpType, cmpTypes, eqTypeX,
  pickyEqType, tcEqType, tcEqKind, tcEqTypeNoKindCheck, tcEqTypeVis,
75
  isSigmaTy, isRhoTy, isRhoExpTy, isOverloadedTy,
Ben Gamari's avatar
Ben Gamari committed
76
  isFloatingTy, isDoubleTy, isFloatTy, isIntTy, isWordTy, isStringTy,
77
  isIntegerTy, isBoolTy, isUnitTy, isCharTy,
78
  isTauTy, isTauTyCon, tcIsTyVarTy, tcIsForAllTy,
79
  isPredTy, isTyVarClassPred, isTyVarExposed, isTyVarUnderDatatype,
80
  checkValidClsArgs, hasTyVarHead,
81
  isRigidEqPred, isRigidTy,
82

83 84
  ---------------------------------
  -- Misc type manipulators
85
  deNoteType, occurCheckExpand, OccCheckResult(..),
Simon Peyton Jones's avatar
Simon Peyton Jones committed
86
  orphNamesOfType, orphNamesOfCo,
87
  orphNamesOfTypes, orphNamesOfCoCon,
88
  getDFunTyKey,
89
  evVarPred_maybe, evVarPred,
90 91

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

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

  -- * Finding "exact" (non-dead) type variables
102 103 104 105
  exactTyCoVarsOfType, exactTyCoVarsOfTypes,

  -- * Extracting bound variables
  allBoundVariables, allBoundVariabless,
106

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

121
  --------------------------------
122 123
  -- Rexported from Kind
  Kind, typeKind,
124
  unliftedTypeKind, liftedTypeKind,
125 126
  constraintKind,
  isLiftedTypeKind, isUnliftedTypeKind, classifiesTypeWithValues,
127

128 129
  --------------------------------
  -- Rexported from Type
130 131
  Type, PredType, ThetaType, TyBinder, VisibilityFlag(..),

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
132
  mkForAllTy, mkForAllTys, mkInvForAllTys, mkSpecForAllTys, mkNamedForAllTy,
133 134 135 136
  mkFunTy, mkFunTys,
  mkTyConApp, mkAppTy, mkAppTys, applyTys,
  mkTyConTy, mkTyVarTy,
  mkTyVarTys,
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
137
  mkNamedBinder,
138

139
  isClassPred, isEqPred, isNomEqPred, isIPPred,
140
  mkClassPred,
141
  isDictLikeTy,
142
  tcSplitDFunTy, tcSplitDFunHead, tcSplitMethodTy,
143 144
  isLevityVar, isLevityPolymorphic, isLevityPolymorphic_maybe,
  isVisibleBinder, isInvisibleBinder,
145

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

162
  isUnliftedType,       -- Source types are always lifted
163 164
  isUnboxedTupleType,   -- Ditto
  isPrimitiveType,
165

166 167 168 169 170 171 172
  coreView,

  tyCoVarsOfType, tyCoVarsOfTypes, closeOverKinds,
  tyCoVarsOfTelescope,
  tyCoVarsOfTypeAcc, tyCoVarsOfTypesAcc,
  tyCoVarsOfTypeDSet, tyCoVarsOfTypesDSet, closeOverKindsDSet,
  tyCoVarsOfTypeList, tyCoVarsOfTypesList,
173

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

179
  pprKind, pprParendKind, pprSigmaType,
180
  pprType, pprParendType, pprTypeApp, pprTyThingCategory,
181 182
  pprTheta, pprThetaArrowTy, pprClassPred,

183
  TypeSize, sizeType, sizeTypes, toposortTyVars
184

185
  ) where
186

187
#include "HsVersions.h"
188

189
-- friends:
190
import Kind
191
import TyCoRep
192 193 194
import Class
import Var
import ForeignCall
195
import VarSet
196
import Coercion
197
import Type
198
import TyCon
199 200

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

import Data.IORef
Austin Seipp's avatar
Austin Seipp committed
222
import Control.Monad (liftM, ap)
223
import Data.Functor.Identity
224

Austin Seipp's avatar
Austin Seipp committed
225 226 227
{-
************************************************************************
*                                                                      *
228
\subsection{Types}
Austin Seipp's avatar
Austin Seipp committed
229 230
*                                                                      *
************************************************************************
231

232
The type checker divides the generic Type world into the
233 234
following more structured beasts:

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

241 242 243 244
        -- 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
245

246 247 248
phi :: theta => rho

rho ::= sigma -> rho
249 250 251 252 253 254 255 256 257 258 259
     |  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.
Austin Seipp's avatar
Austin Seipp committed
260
-}
261

262
type TcTyVar = TyVar    -- Used only during type inference
263
type TcCoVar = CoVar    -- Used only during type inference
264
type TcType = Type      -- A TcType can have mutable type variables
265
type TcTyCoVar = Var    -- Either a TcTyVar or a CoVar
266 267 268 269
        -- 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
270
type TcTyBinder = TyBinder
271

272
-- These types do not have boxy type variables in them
273 274
type TcPredType     = PredType
type TcThetaType    = ThetaType
275
type TcSigmaType    = TcType
276
type TcRhoType      = TcType  -- Note [TcRhoType]
277
type TcTauType      = TcType
278
type TcKind         = Kind
279
type TcTyVarSet     = TyVarSet
280
type TcTyCoVarSet   = TyCoVarSet
281
type TcDTyVarSet    = DTyVarSet
282
type TcDTyCoVarSet  = DTyCoVarSet
283

284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336
-- | An expected type to check against during type-checking.
-- See Note [ExpType] in TcMType, where you'll also find manipulators.
data ExpType = Check TcType
             | Infer Unique  -- for debugging only
                     TcLevel -- See Note [TcLevel of ExpType] in TcMType
                     Kind
                     (IORef (Maybe TcType))

type ExpSigmaType = ExpType
type ExpRhoType   = ExpType

instance Outputable ExpType where
  ppr (Check ty) = ppr ty
  ppr (Infer u lvl ki _)
    = parens (text "Infer" <> braces (ppr u <> comma <> ppr lvl)
              <+> dcolon <+> ppr ki)

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

-- | 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
337
{-
338 339 340 341 342 343 344 345
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

346

Austin Seipp's avatar
Austin Seipp committed
347 348
************************************************************************
*                                                                      *
349
\subsection{TyVarDetails}
Austin Seipp's avatar
Austin Seipp committed
350 351
*                                                                      *
************************************************************************
352

353 354
TyVarDetails gives extra info about type variables, used during type
checking.  It's attached to mutable type variables only.
355 356
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.
357

358 359 360 361
Note [Signature skolems]
~~~~~~~~~~~~~~~~~~~~~~~~
Consider this

362 363 364 365 366 367 368 369 370 371 372 373 374
  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.
375

376 377 378 379 380 381 382 383 384 385
Note [TyVars and TcTyVars]
~~~~~~~~~~~~~~~~~~~~~~~~~~
The Var type has constructors TyVar and TcTyVar.  They are used
as follows:

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

* TyVar: can appear any time.  During type checking they behave
  precisely like (SkolemTv False) = vanillaSkolemTv
Austin Seipp's avatar
Austin Seipp committed
386
-}
387

388
-- A TyVarDetails is inside a TyVar
389
-- See Note [TyVars and TcTyVars]
390
data TcTyVarDetails
391 392 393 394
  = SkolemTv      -- A skolem
       Bool       -- True <=> this skolem type variable can be overlapped
                  --          when looking up instances
                  -- See Note [Binding when looking up instances] in InstEnv
395

396 397 398 399
  | 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

400 401 402
  | RuntimeUnk    -- Stands for an as-yet-unknown type in the GHCi
                  -- interactive context

403 404
  | MetaTv { mtv_info  :: MetaInfo
           , mtv_ref   :: IORef MetaDetails
405
           , mtv_tclvl :: TcLevel }  -- See Note [TcLevel and untouchable type variables]
406

407 408 409 410 411
vanillaSkolemTv, superSkolemTv :: TcTyVarDetails
-- See Note [Binding when looking up instances] in InstEnv
vanillaSkolemTv = SkolemTv False  -- Might be instantiated
superSkolemTv   = SkolemTv True   -- Treat this as a completely distinct type

412
-----------------------------
413
data MetaDetails
414
  = Flexi  -- Flexi type variables unify to become Indirects
415 416
  | Indirect TcType

417
instance Outputable MetaDetails where
418 419
  ppr Flexi         = text "Flexi"
  ppr (Indirect ty) = text "Indirect" <+> ppr ty
420

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
421 422 423 424
data TauTvFlavour
  = VanillaTau
  | WildcardTau    -- ^ A tyvar that originates from a type wildcard.

425
data MetaInfo
426
   = TauTv         -- This MetaTv is an ordinary unification variable
427
                   -- A TauTv is always filled in with a tau-type, which
thomasw's avatar
thomasw committed
428
                   -- never contains any ForAlls.
429

430 431 432 433 434 435
   | 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
436

437 438 439 440
   | 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

441
-------------------------------------
442 443 444 445
-- UserTypeCtxt describes the origin of the polymorphic type
-- in the places where we need to an expression has that type

data UserTypeCtxt
446 447 448 449 450 451 452 453 454 455 456
  = 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
457

458 459
  | InfSigCtxt Name     -- Inferred type for function
  | ExprSigCtxt         -- Expression type signature
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
460
  | TypeAppCtxt         -- Visible type application
461 462
  | ConArgCtxt Name     -- Data constructor argument
  | TySynCtxt Name      -- RHS of a type synonym decl
463 464
  | PatSynCtxt Name     -- Type sig for a pattern synonym
                        --   eg  pattern C :: Int -> T
465 466 467
  | PatSigCtxt          -- Type sig in pattern
                        --   eg  f (x::t) = ...
                        --   or  (x::t, y) = e
468 469
  | RuleSigCtxt Name    -- LHS of a RULE forall
                        --    RULE "foo" forall (x :: a -> a). f (Just x) = ...
470 471 472 473
  | 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
474
  | InstDeclCtxt        -- An instance declaration
475 476
  | SpecInstCtxt        -- SPECIALISE instance pragma
  | ThBrackCtxt         -- Template Haskell type brackets [t| ... |]
477 478 479
  | GenSigCtxt          -- Higher-rank or impredicative situations
                        -- e.g. (f e) where f has a higher-rank type
                        -- We might want to elaborate this
480
  | GhciCtxt            -- GHCi command :kind <type>
481

482 483 484 485 486
  | ClassSCCtxt Name    -- Superclasses of a class
  | SigmaCtxt           -- Theta part of a normal for-all type
                        --      f :: <S> => a -> a
  | DataTyCtxt Name     -- Theta part of a data decl
                        --      data <S> => T a = MkT a
dreixel's avatar
dreixel committed
487

Austin Seipp's avatar
Austin Seipp committed
488
{-
489 490 491
-- Notes re TySynCtxt
-- We allow type synonyms that aren't types; e.g.  type List = []
--
492
-- If the RHS mentions tyvars that aren't in scope, we'll
493
-- quantify over them:
494 495
--      e.g.    type T = a->a
-- will become  type T = forall a. a->a
496
--
497
-- With gla-exts that's right, but for H98 we should complain.
498
-}
499 500


501
{- *********************************************************************
Austin Seipp's avatar
Austin Seipp committed
502
*                                                                      *
503
                Untoucable type variables
Austin Seipp's avatar
Austin Seipp committed
504
*                                                                      *
505
********************************************************************* -}
506

507
newtype TcLevel = TcLevel Int deriving( Eq, Ord )
508
  -- See Note [TcLevel and untouchable type variables] for what this Int is
509
  -- See also Note [TcLevel assignment]
510

Austin Seipp's avatar
Austin Seipp committed
511
{-
512 513
Note [TcLevel and untouchable type variables]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
514
* Each unification variable (MetaTv)
515
  and each Implication
516
  has a level number (of type TcLevel)
517

518 519 520
* INVARIANTS.  In a tree of Implications,

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

523 524
    (MetaTvInv) The level number of a unification variable is
                LESS THAN OR EQUAL TO that of its parent
525 526 527 528 529
                implication

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

530 531 532
* INVARIANT
    (GivenInv)  The free variables of the ic_given of an
                implication are all untouchable; ie their level
533
                numbers are LESS THAN the ic_tclvl of the implication
534

535 536 537
Note [Skolem escape prevention]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We only unify touchable unification variables.  Because of
538 539
(MetaTvInv), there can be no occurrences of the variable further out,
so the unification can't cause the skolems to escape. Example:
540 541 542 543 544 545 546 547 548 549 550 551
     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
552
does not mention 'a') to get
553 554 555 556 557
      (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
558 559
   (F Int ~ uf[0])  /\  [1](forall a. C a => F Int ~ beta[1])
In this example, beta is touchable inside the implication. The
560
first solveSimpleWanteds step leaves 'uf' un-unified. Then we move inside
561
the implication where a new constraint
562 563 564
       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
565
(F Int ~ uf) which will be unified by our final zonking stage and
566
uf will get unified *once more* to (F Int).
567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583

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

   1   Top level
   2     Flatten-meta-vars of level 3
   3   First-level implication constraints
   4     Flatten-meta-vars of level 5
   5   Second-level implication constraints
   ...etc...

The even-numbered levels are for the flatten-meta-variables assigned
at the next level in.  Eg for a second-level implication conststraint
(level 5), the flatten meta-vars are level 4, which makes them untouchable.
The flatten meta-vars could equally well all have level 0, or just NotALevel
since they do not live across implications.
Austin Seipp's avatar
Austin Seipp committed
584
-}
585

586
fmvTcLevel :: TcLevel -> TcLevel
587
-- See Note [TcLevel assignment]
588
fmvTcLevel (TcLevel n) = TcLevel (n-1)
589

590
topTcLevel :: TcLevel
591
-- See Note [TcLevel assignment]
592
topTcLevel = TcLevel 1   -- 1 = outermost level
593

594 595 596 597
isTopTcLevel :: TcLevel -> Bool
isTopTcLevel (TcLevel 1) = True
isTopTcLevel _           = False

598
pushTcLevel :: TcLevel -> TcLevel
599
-- See Note [TcLevel assignment]
600
pushTcLevel (TcLevel us) = TcLevel (us + 2)
601

602 603 604
strictlyDeeperThan :: TcLevel -> TcLevel -> Bool
strictlyDeeperThan (TcLevel tv_tclvl) (TcLevel ctxt_tclvl)
  = tv_tclvl > ctxt_tclvl
605

606 607 608
sameDepthAs :: TcLevel -> TcLevel -> Bool
sameDepthAs (TcLevel ctxt_tclvl) (TcLevel tv_tclvl)
  = ctxt_tclvl == tv_tclvl   -- NB: invariant ctxt_tclvl >= tv_tclvl
609 610
                             --     So <= would be equivalent

611 612 613 614
checkTcLevelInvariant :: TcLevel -> TcLevel -> Bool
-- Checks (MetaTvInv) from Note [TcLevel and untouchable type variables]
checkTcLevelInvariant (TcLevel ctxt_tclvl) (TcLevel tv_tclvl)
  = ctxt_tclvl >= tv_tclvl
615

616 617
instance Outputable TcLevel where
  ppr (TcLevel us) = ppr us
618

Austin Seipp's avatar
Austin Seipp committed
619 620 621
{-
************************************************************************
*                                                                      *
622
                Pretty-printing
Austin Seipp's avatar
Austin Seipp committed
623 624 625
*                                                                      *
************************************************************************
-}
626

627 628
pprTcTyVarDetails :: TcTyVarDetails -> SDoc
-- For debugging
629 630 631 632
pprTcTyVarDetails (SkolemTv True)  = text "ssk"
pprTcTyVarDetails (SkolemTv False) = text "sk"
pprTcTyVarDetails (RuntimeUnk {})  = text "rt"
pprTcTyVarDetails (FlatSkol {})    = text "fsk"
633 634
pprTcTyVarDetails (MetaTv { mtv_info = info, mtv_tclvl = tclvl })
  = pp_info <> colon <> ppr tclvl
635 636
  where
    pp_info = case info of
637 638 639
                TauTv      -> text "tau"
                SigTv      -> text "sig"
                FlatMetaTv -> text "fuv"
640 641

pprUserTypeCtxt :: UserTypeCtxt -> SDoc
642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661
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 (PatSynCtxt c)    = text "the type signature for pattern 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)
662 663 664 665 666 667 668

pprSigCtxt :: UserTypeCtxt -> SDoc -> SDoc -> SDoc
-- (pprSigCtxt ctxt <extra> <type>)
-- prints    In <extra> the type signature for 'f':
--              f :: <type>
-- The <extra> is either empty or "the ambiguity check for"
pprSigCtxt ctxt extra pp_ty
669
  | Just n <- isSigMaybe ctxt
670
  = vcat [ text "In" <+> extra <+> ptext (sLit "the type signature:")
671 672 673
         , nest 2 (pprPrefixOcc n <+> dcolon <+> pp_ty) ]

  | otherwise
674
  = hang (text "In" <+> extra <+> pprUserTypeCtxt ctxt <> colon)
675 676
       2 pp_ty

677 678
  where

679 680 681 682 683 684
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
685

Austin Seipp's avatar
Austin Seipp committed
686 687 688
{-
************************************************************************
*                  *
689
    Finding type family instances
Austin Seipp's avatar
Austin Seipp committed
690 691 692
*                  *
************************************************************************
-}
693

Simon Peyton Jones's avatar
Simon Peyton Jones committed
694 695
-- | Finds outermost type-family applications occuring in a type,
-- after expanding synonyms.
696
tcTyFamInsts :: Type -> [(TyCon, [Type])]
697
tcTyFamInsts ty
698
  | Just exp_ty <- coreView ty  = tcTyFamInsts exp_ty
699
tcTyFamInsts (TyVarTy _)        = []
700
tcTyFamInsts (TyConApp tc tys)
701
  | isTypeFamilyTyCon tc        = [(tc, tys)]
702
  | otherwise                   = concat (map tcTyFamInsts tys)
703
tcTyFamInsts (LitTy {})         = []
704 705
tcTyFamInsts (ForAllTy bndr ty) = tcTyFamInsts (binderType bndr)
                                  ++ tcTyFamInsts ty
706
tcTyFamInsts (AppTy ty1 ty2)    = tcTyFamInsts ty1 ++ tcTyFamInsts ty2
707 708 709
tcTyFamInsts (CastTy ty _)      = tcTyFamInsts ty
tcTyFamInsts (CoercionTy _)     = []  -- don't count tyfams in coercions,
                                      -- as they never get normalized, anyway
Austin Seipp's avatar
Austin Seipp committed
710 711 712
{-
************************************************************************
*                  *
713
          The "exact" free variables of a type
Austin Seipp's avatar
Austin Seipp committed
714 715
*                  *
************************************************************************
716 717 718 719 720

Note [Silly type synonym]
~~~~~~~~~~~~~~~~~~~~~~~~~
Consider
  type T a = Int
721
What are the free tyvars of (T x)?  Empty, of course!
722 723 724 725 726 727 728 729 730 731
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.

732
exactTyCoVarsOfType is used by the type checker to figure out exactly
733 734 735 736 737 738
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
739
if we have an application like (f "x") we get a confusing error message
740
involving Any.  So the conclusion is this: when generalising
741 742
  - at top level use tyCoVarsOfType
  - in nested bindings use exactTyCoVarsOfType
743
See Trac #1813 for example.
Austin Seipp's avatar
Austin Seipp committed
744
-}
745

746
exactTyCoVarsOfType :: Type -> TyCoVarSet
747 748
-- Find the free type variables (of any kind)
-- but *expand* type synonyms.  See Note [Silly type synonym] above.
749
exactTyCoVarsOfType ty
750 751
  = go ty
  where
752
    go ty | Just ty' <- coreView ty = go ty'  -- This is the key line
753
    go (TyVarTy tv)         = unitVarSet tv
754
    go (TyConApp _ tys)     = exactTyCoVarsOfTypes tys
755
    go (LitTy {})           = emptyVarSet
756
    go (AppTy fun arg)      = go fun `unionVarSet` go arg
757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788
    go (ForAllTy bndr ty)   = delBinderVar (go ty) bndr `unionVarSet` go (binderType bndr)
    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
789

790 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817
{-
************************************************************************
*                  *
          Bound variables in a type
*                  *
************************************************************************
-}

-- | Find all variables bound anywhere in a type.
-- See also Note [Scope-check inferred kinds] in TcHsType
allBoundVariables :: Type -> TyVarSet
allBoundVariables ty = runFVSet $ go ty
  where
    go :: Type -> FV
    go (TyVarTy tv)     = go (tyVarKind tv)
    go (TyConApp _ tys) = mapUnionFV go tys
    go (AppTy t1 t2)    = go t1 `unionFV` go t2
    go (ForAllTy (Anon t1) t2) = go t1 `unionFV` go t2
    go (ForAllTy (Named tv _) t2) = oneVar tv `unionFV`
                                    go (tyVarKind tv) `unionFV` go t2
    go (LitTy {})       = noVars
    go (CastTy ty _)    = go ty
    go (CoercionTy {})  = noVars
      -- any types mentioned in a coercion should also be mentioned in
      -- a type.

allBoundVariabless :: [Type] -> TyVarSet
allBoundVariabless = mapUnionVarSet allBoundVariables
818

Austin Seipp's avatar
Austin Seipp committed
819 820 821
{-
************************************************************************
*                                                                      *
822
                Predicates
Austin Seipp's avatar
Austin Seipp committed
823 824 825
*                                                                      *
************************************************************************
-}
826

827 828
isTouchableOrFmv :: TcLevel -> TcTyVar -> Bool
isTouchableOrFmv ctxt_tclvl tv
829
  = case tcTyVarDetails tv of
830 831 832
      MetaTv { mtv_tclvl = tv_tclvl, mtv_info = info }
        -> ASSERT2( checkTcLevelInvariant ctxt_tclvl tv_tclvl,
                    ppr tv $$ ppr tv_tclvl $$ ppr ctxt_tclvl )
833 834
           case info of
             FlatMetaTv -> True
835
             _          -> tv_tclvl `sameDepthAs` ctxt_tclvl
836 837
      _          -> False

838 839
isTouchableMetaTyVar :: TcLevel -> TcTyVar -> Bool
isTouchableMetaTyVar ctxt_tclvl tv
840 841
  | isTyVar tv
  = case tcTyVarDetails tv of
842 843 844 845
      MetaTv { mtv_tclvl = tv_tclvl }
        -> ASSERT2( checkTcLevelInvariant ctxt_tclvl tv_tclvl,
                    ppr tv $$ ppr tv_tclvl $$ ppr ctxt_tclvl )
           tv_tclvl `sameDepthAs` ctxt_tclvl
846
      _ -> False
847
  | otherwise = False
848

849 850
isFloatedTouchableMetaTyVar :: TcLevel -> TcTyVar -> Bool
isFloatedTouchableMetaTyVar ctxt_tclvl tv
851 852
  | isTyVar tv
  = case tcTyVarDetails tv of
853
      MetaTv { mtv_tclvl = tv_tclvl } -> tv_tclvl `strictlyDeeperThan` ctxt_tclvl
854
      _ -> False
855
  | otherwise = False
856

857
isImmutableTyVar :: TyVar -> Bool
858 859 860 861
isImmutableTyVar tv
  | isTcTyVar tv = isSkolemTyVar tv
  | otherwise    = True

862
isTyConableTyVar, isSkolemTyVar, isOverlappableTyVar,
Austin Seipp's avatar
Austin Seipp committed
863
  isMetaTyVar, isAmbiguousTyVar,
864
  isFmvTyVar, isFskTyVar, isFlattenTyVar :: TcTyVar -> Bool
865

866 867 868 869
isTyConableTyVar tv
        -- True of a meta-type variable that can be filled in
        -- with a type constructor application; in particular,
        -- not a SigTv
870 871
  | isTyVar tv
  = case tcTyVarDetails tv of
872 873
        MetaTv { mtv_info = SigTv } -> False
        _                           -> True
874
  | otherwise = True
875

876
isFmvTyVar tv
877
  = case tcTyVarDetails tv of
878 879 880 881 882
        MetaTv { mtv_info = FlatMetaTv } -> True
        _                                -> False

-- | True of both given and wanted flatten-skolems (fak and usk)
isFlattenTyVar tv
883
  = case tcTyVarDetails tv of
884 885 886 887 888 889
        FlatSkol {}                      -> True
        MetaTv { mtv_info = FlatMetaTv } -> True
        _                                -> False

-- | True of FlatSkol skolems only
isFskTyVar tv
890
  = case tcTyVarDetails tv of