Type.hs 135 KB
Newer Older
1 2 3 4
-- (c) The University of Glasgow 2006
-- (c) The GRASP/AQUA Project, Glasgow University, 1998
--
-- Type - public interface
5

6
{-# LANGUAGE CPP, FlexibleContexts, PatternSynonyms, ViewPatterns #-}
7
{-# OPTIONS_GHC -fno-warn-orphans #-}
8
{-# OPTIONS_GHC -Wno-incomplete-record-updates #-}
Ian Lynagh's avatar
Ian Lynagh committed
9

batterseapower's avatar
batterseapower committed
10
-- | Main functions for manipulating types and type-related things
Sylvain Henry's avatar
Sylvain Henry committed
11
module GHC.Core.Type (
ian@well-typed.com's avatar
ian@well-typed.com committed
12
        -- Note some of this is just re-exports from TyCon..
13

batterseapower's avatar
batterseapower committed
14
        -- * Main data types representing Types
ian@well-typed.com's avatar
ian@well-typed.com committed
15 16
        -- $type_classification

batterseapower's avatar
batterseapower committed
17
        -- $representation_types
Sylvain Henry's avatar
Sylvain Henry committed
18
        Type, ArgFlag(..), AnonArgFlag(..),
Gert-Jan Bottu's avatar
Gert-Jan Bottu committed
19
        Specificity(..),
Simon Peyton Jones's avatar
Simon Peyton Jones committed
20
        KindOrType, PredType, ThetaType,
Ningning Xie's avatar
Ningning Xie committed
21
        Var, TyVar, isTyVar, TyCoVar, TyCoBinder, TyCoVarBinder, TyVarBinder,
Krzysztof Gogolewski's avatar
Krzysztof Gogolewski committed
22
        Mult, Scaled,
23
        KnotTied,
24

batterseapower's avatar
batterseapower committed
25
        -- ** Constructing and deconstructing types
26
        mkTyVarTy, mkTyVarTys, getTyVar, getTyVar_maybe, repGetTyVar_maybe,
Ningning Xie's avatar
Ningning Xie committed
27
        getCastedTyVar_maybe, tyVarKind, varType,
28

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
29
        mkAppTy, mkAppTys, splitAppTy, splitAppTys, repSplitAppTys,
30
        splitAppTy_maybe, repSplitAppTy_maybe, tcRepSplitAppTy_maybe,
31

32
        mkFunTy, mkVisFunTy, mkInvisFunTy,
Krzysztof Gogolewski's avatar
Krzysztof Gogolewski committed
33 34 35
        mkVisFunTys,
        mkVisFunTyMany, mkInvisFunTyMany,
        mkVisFunTysMany, mkInvisFunTysMany,
Simon Peyton Jones's avatar
Simon Peyton Jones committed
36
        splitFunTy, splitFunTy_maybe,
37
        splitFunTys, funResultTy, funArgTy,
38

ian@well-typed.com's avatar
ian@well-typed.com committed
39
        mkTyConApp, mkTyConTy,
40 41
        tyConAppTyCon_maybe, tyConAppTyConPicky_maybe,
        tyConAppArgs_maybe, tyConAppTyCon, tyConAppArgs,
Krzysztof Gogolewski's avatar
Krzysztof Gogolewski committed
42
        splitTyConApp_maybe, splitTyConApp, tyConAppArgN,
Simon Peyton Jones's avatar
Simon Peyton Jones committed
43
        tcSplitTyConApp_maybe,
44 45 46
        splitListTyConApp_maybe,
        repSplitTyConApp_maybe,

Gert-Jan Bottu's avatar
Gert-Jan Bottu committed
47
        mkForAllTy, mkForAllTys, mkInvisForAllTys, mkTyCoInvForAllTys,
48
        mkSpecForAllTy, mkSpecForAllTys,
Ningning Xie's avatar
Ningning Xie committed
49
        mkVisForAllTys, mkTyCoInvForAllTy,
Gert-Jan Bottu's avatar
Gert-Jan Bottu committed
50
        mkInfForAllTy, mkInfForAllTys,
51 52 53 54 55
        splitForAllTyCoVars,
        splitForAllReqTVBinders, splitForAllInvisTVBinders,
        splitForAllTyCoVarBinders,
        splitForAllTyCoVar_maybe, splitForAllTyCoVar,
        splitForAllTyVar_maybe, splitForAllCoVar_maybe,
Simon Peyton Jones's avatar
Simon Peyton Jones committed
56
        splitPiTy_maybe, splitPiTy, splitPiTys,
Simon Peyton Jones's avatar
Simon Peyton Jones committed
57 58
        mkTyConBindersPreferAnon,
        mkPiTy, mkPiTys,
59
        piResultTy, piResultTys,
60
        applyTysX, dropForAlls,
61
        mkFamilyTyConApp,
62
        buildSynTyCon,
63

64 65
        mkNumLitTy, isNumLitTy,
        mkStrLitTy, isStrLitTy,
66
        isLitTy,
67

68 69
        isPredTy,

70
        getRuntimeRep_maybe, kindRep_maybe, kindRep,
Ben Gamari's avatar
Ben Gamari committed
71

Simon Peyton Jones's avatar
Simon Peyton Jones committed
72
        mkCastTy, mkCoercionTy, splitCastTy_maybe,
73

74
        userTypeError_maybe, pprUserTypeErrorTy,
75

76
        coAxNthLHS,
77
        stripCoercionTy,
78

79
        splitInvisPiTys, splitInvisPiTysN,
80 81
        invisibleTyBndrCount,
        filterOutInvisibleTypes, filterOutInferredTypes,
82 83
        partitionInvisibleTypes, partitionInvisibles,
        tyConArgFlags, appTyArgFlags,
84

85
        -- ** Analyzing types
86
        TyCoMapper(..), mapTyCo, mapTyCoX,
87
        TyCoFolder(..), foldTyCo,
ian@well-typed.com's avatar
ian@well-typed.com committed
88 89 90 91

        -- (Newtypes)
        newTyConInstRhs,

92
        -- ** Binders
93
        sameVis,
Ningning Xie's avatar
Ningning Xie committed
94
        mkTyCoVarBinder, mkTyCoVarBinders,
Krzysztof Gogolewski's avatar
Krzysztof Gogolewski committed
95
        mkTyVarBinder, mkTyVarBinders,
Gert-Jan Bottu's avatar
Gert-Jan Bottu committed
96
        tyVarSpecToBinders,
97
        mkAnonBinder,
98
        isAnonTyCoBinder,
Ningning Xie's avatar
Ningning Xie committed
99 100 101
        binderVar, binderVars, binderType, binderArgFlag,
        tyCoBinderType, tyCoBinderVar_maybe,
        tyBinderType,
Simon Peyton Jones's avatar
Simon Peyton Jones committed
102
        binderRelevantType_maybe,
103 104
        isVisibleArgFlag, isInvisibleArgFlag, isVisibleBinder,
        isInvisibleBinder, isNamedBinder,
Ningning Xie's avatar
Ningning Xie committed
105
        tyConBindersTyCoBinders,
106

ian@well-typed.com's avatar
ian@well-typed.com committed
107
        -- ** Common type constructors
Krzysztof Gogolewski's avatar
Krzysztof Gogolewski committed
108
        funTyCon, unrestrictedFunTyCon,
109

batterseapower's avatar
batterseapower committed
110
        -- ** Predicates on types
111
        isTyVarTy, isFunTy, isCoercionTy,
112
        isCoercionTy_maybe, isForAllTy,
Ningning Xie's avatar
Ningning Xie committed
113
        isForAllTy_ty, isForAllTy_co,
114
        isPiTy, isTauTy, isFamFreeTy,
Simon Peyton Jones's avatar
Simon Peyton Jones committed
115
        isCoVarType, isAtomicTy,
batterseapower's avatar
batterseapower committed
116

lukemaurer's avatar
lukemaurer committed
117
        isValidJoinPointType,
Ben Gamari's avatar
Ben Gamari committed
118
        tyConAppNeedsKindSig,
lukemaurer's avatar
lukemaurer committed
119

120 121
        -- *** Levity and boxity
        isLiftedType_maybe,
122
        isLiftedTypeKind, isUnliftedTypeKind, pickyIsLiftedTypeKind,
123
        isLiftedRuntimeRep, isUnliftedRuntimeRep,
Andrew Martin's avatar
Andrew Martin committed
124
        isLiftedLevity, isUnliftedLevity,
125
        isUnliftedType, mightBeUnliftedType, isUnboxedTupleType, isUnboxedSumType,
126
        isAlgType, isDataFamilyAppType,
ian@well-typed.com's avatar
ian@well-typed.com committed
127
        isPrimitiveType, isStrictType,
128 129
        isRuntimeRepTy, isRuntimeRepVar, isRuntimeRepKindedTy,
        dropRuntimeRepArgs,
130
        getRuntimeRep,
131

132
        -- * Multiplicity
Krzysztof Gogolewski's avatar
Krzysztof Gogolewski committed
133 134

        isMultiplicityTy, isMultiplicityVar,
135 136 137 138
        unrestricted, linear, tymult,
        mkScaled, irrelevantMult, scaledSet,
        pattern One, pattern Many,
        isOneDataConTy, isManyDataConTy,
Krzysztof Gogolewski's avatar
Krzysztof Gogolewski committed
139 140
        isLinearType,

ian@well-typed.com's avatar
ian@well-typed.com committed
141
        -- * Main data types representing Kinds
142
        Kind,
batterseapower's avatar
batterseapower committed
143 144

        -- ** Finding the kind of a type
145
        typeKind, tcTypeKind, isTypeLevPoly, resultIsLevPoly,
146
        tcIsLiftedTypeKind, tcIsConstraintKind, tcReturnsConstraintKind,
147
        tcIsRuntimeTypeKind,
ian@well-typed.com's avatar
ian@well-typed.com committed
148

149
        -- ** Common Kind
150
        liftedTypeKind,
batterseapower's avatar
batterseapower committed
151

ian@well-typed.com's avatar
ian@well-typed.com committed
152
        -- * Type free variables
153
        tyCoFVsOfType, tyCoFVsBndr, tyCoFVsVarBndr, tyCoFVsVarBndrs,
Simon Peyton Jones's avatar
Simon Peyton Jones committed
154
        tyCoVarsOfType, tyCoVarsOfTypes,
155 156
        tyCoVarsOfTypeDSet,
        coVarsOfType,
Tobias Dammers's avatar
Tobias Dammers committed
157 158
        coVarsOfTypes,

159
        anyFreeVarsOfType, anyFreeVarsOfTypes,
Richard Eisenberg's avatar
Richard Eisenberg committed
160
        noFreeVarsOfType,
161
        splitVisVarsOfType, splitVisVarsOfTypes,
ian@well-typed.com's avatar
ian@well-typed.com committed
162
        expandTypeSynonyms,
163
        typeSize, occCheckExpand,
164

165
        -- ** Closing over kinds
Simon Peyton Jones's avatar
Simon Peyton Jones committed
166
        closeOverKindsDSet, closeOverKindsList,
167 168
        closeOverKinds,

169
        -- * Well-scoped lists of variables
170 171
        scopedSort, tyCoVarsOfTypeWellScoped,
        tyCoVarsOfTypesWellScoped,
172

ian@well-typed.com's avatar
ian@well-typed.com committed
173
        -- * Type comparison
niteria's avatar
niteria committed
174 175
        eqType, eqTypeX, eqTypes, nonDetCmpType, nonDetCmpTypes, nonDetCmpTypeX,
        nonDetCmpTypesX, nonDetCmpTc,
176
        eqVarBndrs,
177

ian@well-typed.com's avatar
ian@well-typed.com committed
178
        -- * Forcing evaluation of types
batterseapower's avatar
batterseapower committed
179
        seqType, seqTypes,
180

batterseapower's avatar
batterseapower committed
181
        -- * Other views onto Types
Ben Gamari's avatar
Ben Gamari committed
182
        coreView, tcView,
batterseapower's avatar
batterseapower committed
183

184
        tyConsOfType,
batterseapower's avatar
batterseapower committed
185

ian@well-typed.com's avatar
ian@well-typed.com committed
186 187
        -- * Main type substitution data types
        TvSubstEnv,     -- Representation widely visible
188
        TCvSubst(..),    -- Representation visible to a few friends
ian@well-typed.com's avatar
ian@well-typed.com committed
189 190

        -- ** Manipulating type substitutions
191
        emptyTvSubstEnv, emptyTCvSubst, mkEmptyTCvSubst,
ian@well-typed.com's avatar
ian@well-typed.com committed
192

niteria's avatar
niteria committed
193
        mkTCvSubst, zipTvSubst, mkTvSubstPrs,
Ningning Xie's avatar
Ningning Xie committed
194
        zipTCvSubst,
195
        notElemTCvSubst,
196
        getTvSubstEnv, setTvSubstEnv,
197
        zapTCvSubst, getTCvInScope, getTCvSubstRangeFVs,
198
        extendTCvInScope, extendTCvInScopeList, extendTCvInScopeSet,
199
        extendTCvSubst, extendCvSubst,
Richard Eisenberg's avatar
Richard Eisenberg committed
200
        extendTvSubst, extendTvSubstBinderAndInScope,
201
        extendTvSubstList, extendTvSubstAndInScope,
Ningning Xie's avatar
Ningning Xie committed
202
        extendTCvSubstList,
203
        extendTvSubstWithClone,
Ningning Xie's avatar
Ningning Xie committed
204
        extendTCvSubstWithClone,
205 206
        isInScope, composeTCvSubstEnv, composeTCvSubst, zipTyEnv, zipCoEnv,
        isEmptyTCvSubst, unionTCvSubst,
207

ian@well-typed.com's avatar
ian@well-typed.com committed
208
        -- ** Performing substitution on types and kinds
Krzysztof Gogolewski's avatar
Krzysztof Gogolewski committed
209
        substTy, substTys, substScaledTy, substScaledTys, substTyWith, substTysWith, substTheta,
210
        substTyAddInScope,
Krzysztof Gogolewski's avatar
Krzysztof Gogolewski committed
211 212
        substTyUnchecked, substTysUnchecked, substScaledTyUnchecked, substScaledTysUnchecked,
        substThetaUnchecked, substTyWithUnchecked,
213
        substCoUnchecked, substCoWithUnchecked,
Simon Peyton Jones's avatar
Simon Peyton Jones committed
214
        substTyVarBndr, substTyVarBndrs, substTyVar, substTyVars,
Ningning Xie's avatar
Ningning Xie committed
215
        substVarBndr, substVarBndrs,
216
        cloneTyVarBndr, cloneTyVarBndrs, lookupTyVar,
217

Simon Peyton Jones's avatar
Simon Peyton Jones committed
218 219 220 221
        -- * Tidying type related things up for printing
        tidyType,      tidyTypes,
        tidyOpenType,  tidyOpenTypes,
        tidyOpenKind,
Ningning Xie's avatar
Ningning Xie committed
222
        tidyVarBndr, tidyVarBndrs, tidyFreeTyCoVars,
223
        tidyOpenTyCoVar, tidyOpenTyCoVars,
Ningning Xie's avatar
Ningning Xie committed
224
        tidyTyCoVarOcc,
Simon Peyton Jones's avatar
Simon Peyton Jones committed
225
        tidyTopType,
226
        tidyKind,
227 228 229 230 231 232
        tidyTyCoVarBinder, tidyTyCoVarBinders,

        -- * Kinds
        isConstraintKindCon,
        classifiesTypeWithValues,
        isKindLevPoly
233
    ) where
234

235 236
#include "HsVersions.h"

237
import GHC.Prelude
238

Sylvain Henry's avatar
Sylvain Henry committed
239
import GHC.Types.Basic
lukemaurer's avatar
lukemaurer committed
240

Sylvain Henry's avatar
Sylvain Henry committed
241
-- We import the representation and primitive functions from GHC.Core.TyCo.Rep.
242 243
-- Many things are reexported, but not the representation!

Sylvain Henry's avatar
Sylvain Henry committed
244 245 246 247
import GHC.Core.TyCo.Rep
import GHC.Core.TyCo.Subst
import GHC.Core.TyCo.Tidy
import GHC.Core.TyCo.FVs
248

249
-- friends:
Sylvain Henry's avatar
Sylvain Henry committed
250 251 252 253
import GHC.Types.Var
import GHC.Types.Var.Env
import GHC.Types.Var.Set
import GHC.Types.Unique.Set
254

Sylvain Henry's avatar
Sylvain Henry committed
255
import GHC.Core.TyCon
Sylvain Henry's avatar
Sylvain Henry committed
256 257
import GHC.Builtin.Types.Prim
import {-# SOURCE #-} GHC.Builtin.Types
258
                                 ( naturalTy, listTyCon
259
                                 , typeSymbolKind, liftedTypeKind
Krzysztof Gogolewski's avatar
Krzysztof Gogolewski committed
260
                                 , constraintKind
261 262
                                 , unrestrictedFunTyCon
                                 , manyDataConTy, oneDataConTy )
Sylvain Henry's avatar
Sylvain Henry committed
263
import GHC.Types.Name( Name )
Sylvain Henry's avatar
Sylvain Henry committed
264
import GHC.Builtin.Names
Sylvain Henry's avatar
Sylvain Henry committed
265 266 267 268 269 270
import GHC.Core.Coercion.Axiom
import {-# SOURCE #-} GHC.Core.Coercion
   ( mkNomReflCo, mkGReflCo, mkReflCo
   , mkTyConAppCo, mkAppCo, mkCoVarCo, mkAxiomRuleCo
   , mkForAllCo, mkFunCo, mkAxiomInstCo, mkUnivCo
   , mkSymCo, mkTransCo, mkNthCo, mkLRCo, mkInstCo
271
   , mkKindCo, mkSubCo
Sylvain Henry's avatar
Sylvain Henry committed
272 273 274
   , decomposePiCos, coercionKind, coercionLKind
   , coercionRKind, coercionType
   , isReflexiveCo, seqCo )
275

276
-- others
277 278 279
import GHC.Utils.Misc
import GHC.Utils.FV
import GHC.Utils.Outputable
280
import GHC.Utils.Panic
281 282 283
import GHC.Data.FastString
import GHC.Data.Pair
import GHC.Data.List.SetOps
Sylvain Henry's avatar
Sylvain Henry committed
284
import GHC.Types.Unique ( nonDetCmpUnique )
simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
285

286
import GHC.Data.Maybe   ( orElse, expectJust )
287
import Data.Maybe       ( isJust )
288
import Control.Monad    ( guard )
289

batterseapower's avatar
batterseapower committed
290 291
-- $type_classification
-- #type_classification#
ian@well-typed.com's avatar
ian@well-typed.com committed
292
--
batterseapower's avatar
batterseapower committed
293
-- Types are one of:
ian@well-typed.com's avatar
ian@well-typed.com committed
294
--
batterseapower's avatar
batterseapower committed
295
-- [Unboxed]            Iff its representation is other than a pointer
ian@well-typed.com's avatar
ian@well-typed.com committed
296 297
--                      Unboxed types are also unlifted.
--
batterseapower's avatar
batterseapower committed
298
-- [Lifted]             Iff it has bottom as an element.
ian@well-typed.com's avatar
ian@well-typed.com committed
299 300 301 302 303 304
--                      Closures always have lifted types: i.e. any
--                      let-bound identifier in Core must have a lifted
--                      type. Operationally, a lifted object is one that
--                      can be entered.
--                      Only lifted types may be unified with a type variable.
--
batterseapower's avatar
batterseapower committed
305
-- [Algebraic]          Iff it is a type with one or more constructors, whether
ian@well-typed.com's avatar
ian@well-typed.com committed
306 307 308 309 310 311
--                      declared with @data@ or @newtype@.
--                      An algebraic type is one that can be deconstructed
--                      with a case expression. This is /not/ the same as
--                      lifted types, because we also include unboxed
--                      tuples in this classification.
--
batterseapower's avatar
batterseapower committed
312
-- [Data]               Iff it is a type declared with @data@, or a boxed tuple.
ian@well-typed.com's avatar
ian@well-typed.com committed
313
--
batterseapower's avatar
batterseapower committed
314
-- [Primitive]          Iff it is a built-in type that can't be expressed in Haskell.
ian@well-typed.com's avatar
ian@well-typed.com committed
315
--
batterseapower's avatar
batterseapower committed
316 317
-- Currently, all primitive types are unlifted, but that's not necessarily
-- the case: for example, @Int@ could be primitive.
ian@well-typed.com's avatar
ian@well-typed.com committed
318
--
batterseapower's avatar
batterseapower committed
319 320 321
-- Some primitive types are unboxed, such as @Int#@, whereas some are boxed
-- but unlifted (such as @ByteArray#@).  The only primitive types that we
-- classify as algebraic are the unboxed tuples.
ian@well-typed.com's avatar
ian@well-typed.com committed
322
--
batterseapower's avatar
batterseapower committed
323
-- Some examples of type classifications that may make this a bit clearer are:
ian@well-typed.com's avatar
ian@well-typed.com committed
324
--
batterseapower's avatar
batterseapower committed
325
-- @
326
-- Type          primitive       boxed           lifted          algebraic
batterseapower's avatar
batterseapower committed
327
-- -----------------------------------------------------------------------------
328 329 330 331 332 333
-- Int#          Yes             No              No              No
-- ByteArray#    Yes             Yes             No              No
-- (\# a, b \#)  Yes             No              No              Yes
-- (\# a | b \#) Yes             No              No              Yes
-- (  a, b  )    No              Yes             Yes             Yes
-- [a]           No              Yes             Yes             Yes
batterseapower's avatar
batterseapower committed
334 335 336 337 338
-- @

-- $representation_types
-- A /source type/ is a type that is a separate type as far as the type checker is
-- concerned, but which has a more low-level representation as far as Core-to-Core
batterseapower's avatar
batterseapower committed
339
-- passes and the rest of the back end is concerned.
batterseapower's avatar
batterseapower committed
340 341 342
--
-- You don't normally have to worry about this, as the utility functions in
-- this module will automatically convert a source into a representation type
Ningning Xie's avatar
Ningning Xie committed
343
-- if they are spotted, to the best of its abilities. If you don't want this
batterseapower's avatar
batterseapower committed
344
-- to happen, use the equivalent functions from the "TcType" module.
345

346 347 348
{-
************************************************************************
*                                                                      *
ian@well-typed.com's avatar
ian@well-typed.com committed
349
                Type representation
350 351
*                                                                      *
************************************************************************
Ben Gamari's avatar
Ben Gamari committed
352 353 354

Note [coreView vs tcView]
~~~~~~~~~~~~~~~~~~~~~~~~~
355 356
So far as the typechecker is concerned, 'Constraint' and 'TYPE
LiftedRep' are distinct kinds.
Ben Gamari's avatar
Ben Gamari committed
357 358 359

But in Core these two are treated as identical.

360 361
We implement this by making 'coreView' convert 'Constraint' to 'TYPE
LiftedRep' on the fly.  The function tcView (used in the type checker)
362 363 364
does not do this. Accordingly, tcView is used in type-checker-oriented
functions (including the pure unifier, used in instance resolution),
while coreView is used during e.g. optimisation passes.
Ben Gamari's avatar
Ben Gamari committed
365

366
See also #11715, which tracks removing this inconsistency.
Ben Gamari's avatar
Ben Gamari committed
367

368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383
The inconsistency actually leads to a potential soundness bug, in that
Constraint and Type are considered *apart* by the type family engine.
To wit, we can write

  type family F a
  type instance F Type = Bool
  type instance F Constraint = Int

and (because Type ~# Constraint in Core), thus build a coercion between
Int and Bool. I (Richard E) conjecture that this never happens in practice,
but it's very uncomfortable. This, essentially, is the root problem
underneath #11715, which is quite resistant to an easy fix. The best
idea is to have roles in kind coercions, but that has yet to be implemented.
See also "A Role for Dependent Types in Haskell", ICFP 2019, which describes
how roles in kinds might work out.

384
-}
385

Ben Gamari's avatar
Ben Gamari committed
386
-- | Gives the typechecker view of a type. This unwraps synonyms but
387 388
-- leaves 'Constraint' alone. c.f. 'coreView', which turns 'Constraint' into
-- 'Type'. Returns 'Nothing' if no unwrapping happens.
389
-- See also Note [coreView vs tcView]
Ben Gamari's avatar
Ben Gamari committed
390
tcView :: Type -> Maybe Type
391 392 393
tcView (TyConApp tc tys)
  | res@(Just _) <- expandSynTyConApp_maybe tc tys
  = res
Ben Gamari's avatar
Ben Gamari committed
394
tcView _ = Nothing
395 396
-- See Note [Inlining coreView].
{-# INLINE tcView #-}
397

398
coreView :: Type -> Maybe Type
399
-- ^ This function strips off the /top layer only/ of a type synonym
400
-- application (if any) its underlying representation type.
401 402
-- Returns 'Nothing' if there is nothing to look through.
-- This function considers 'Constraint' to be a synonym of @Type@.
403 404 405 406
--
-- By being non-recursive and inlined, this case analysis gets efficiently
-- joined onto the case analysis that the caller is already doing
coreView ty@(TyConApp tc tys)
407 408
  | res@(Just _) <- expandSynTyConApp_maybe tc tys
  = res
409 410 411 412 413 414 415 416

  -- At the Core level, Constraint = Type
  -- See Note [coreView vs tcView]
  | isConstraintKindCon tc
  = ASSERT2( null tys, ppr ty )
    Just liftedTypeKind

coreView _ = Nothing
417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457
-- See Note [Inlining coreView].
{-# INLINE coreView #-}

-----------------------------------------------

-- | @expandSynTyConApp_maybe tc tys@ expands the RHS of type synonym @tc@
-- instantiated at arguments @tys@, or returns 'Nothing' if @tc@ is not a
-- synonym.
expandSynTyConApp_maybe :: TyCon -> [Type] -> Maybe Type
expandSynTyConApp_maybe tc tys
  | Just (tvs, rhs) <- synTyConDefn_maybe tc
  , tys `lengthAtLeast` arity
  = Just (expand_syn arity tvs rhs tys)
  | otherwise
  = Nothing
  where
    arity = tyConArity tc
-- Without this INLINE the call to expandSynTyConApp_maybe in coreView
-- will result in an avoidable allocation.
{-# INLINE expandSynTyConApp_maybe #-}

-- | A helper for 'expandSynTyConApp_maybe' to avoid inlining this cold path
-- into call-sites.
expand_syn :: Int      -- ^ the arity of the synonym
           -> [TyVar]  -- ^ the variables bound by the synonym
           -> Type     -- ^ the RHS of the synonym
           -> [Type]   -- ^ the type arguments the synonym is instantiated at.
           -> Type
expand_syn arity tvs rhs tys
  | tys `lengthExceeds` arity = mkAppTys rhs' (drop arity tys)
  | otherwise                 = rhs'
  where
    rhs' = substTy (mkTvSubstPrs (tvs `zip` tys)) rhs
               -- The free vars of 'rhs' should all be bound by 'tenv', so it's
               -- ok to use 'substTy' here (which is what expandSynTyConApp_maybe does).
               -- See also Note [The substitution invariant] in GHC.Core.TyCo.Subst.
               -- Its important to use mkAppTys, rather than (foldl AppTy),
               -- because the function part might well return a
               -- partially-applied type constructor; indeed, usually will!
-- We never want to inline this cold-path.
{-# INLINE expand_syn #-}
458

459 460 461 462 463 464 465 466 467 468 469
coreFullView :: Type -> Type
-- ^ Iterates 'coreView' until there is no more to synonym to expand.
-- See Note [Inlining coreView].
coreFullView ty@(TyConApp tc _)
  | isTypeSynonymTyCon tc || isConstraintKindCon tc = go ty
  where
    go ty
      | Just ty' <- coreView ty = go ty'
      | otherwise = ty

coreFullView ty = ty
470
{-# INLINE coreFullView #-}
471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489

{- Note [Inlining coreView] in GHC.Core.Type
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
It is very common to have a function

  f :: Type -> ...
  f ty | Just ty' <- coreView ty = f ty'
  f (TyVarTy ...) = ...
  f ...           = ...

If f is not otherwise recursive, the initial call to coreView
causes f to become recursive, which kills the possibility of
inlining. Instead, for non-recursive functions, we prefer to
use coreFullView, which guarantees to unwrap top-level type
synonyms. It can be inlined and is efficient and non-allocating
in its fast path. For this to really be fast, all calls made
on its fast path must also be inlined, linked back to this Note.
-}

490 491 492 493 494
-----------------------------------------------
expandTypeSynonyms :: Type -> Type
-- ^ Expand out all type synonyms.  Actually, it'd suffice to expand out
-- just the ones that discard type variables (e.g.  type Funny a = Int)
-- But we don't know which those are currently, so we just expand all.
495 496 497
--
-- 'expandTypeSynonyms' only expands out type synonyms mentioned in the type,
-- not in the kinds of any TyCon or TyVar mentioned in the type.
498 499
--
-- Keep this synchronized with 'synonymTyConsOfType'
ian@well-typed.com's avatar
ian@well-typed.com committed
500
expandTypeSynonyms ty
501
  = go (mkEmptyTCvSubst in_scope) ty
502
  where
503 504
    in_scope = mkInScopeSet (tyCoVarsOfType ty)

505
    go subst (TyConApp tc tys)
506 507 508 509 510 511 512 513
      | Just (tenv, rhs, tys') <- expandSynTyCon_maybe tc expanded_tys
      = let subst' = mkTvSubst in_scope (mkVarEnv tenv)
            -- Make a fresh substitution; rhs has nothing to
            -- do with anything that has happened so far
            -- NB: if you make changes here, be sure to build an
            --     /idempotent/ substitution, even in the nested case
            --        type T a b = a -> b
            --        type S x y = T y x
514
            -- (#11665)
515
        in  mkAppTys (go subst' rhs) tys'
516
      | otherwise
517 518 519 520
      = TyConApp tc expanded_tys
      where
        expanded_tys = (map (go subst) tys)

521 522 523
    go _     (LitTy l)     = LitTy l
    go subst (TyVarTy tv)  = substTyVar subst tv
    go subst (AppTy t1 t2) = mkAppTy (go subst t1) (go subst t2)
Krzysztof Gogolewski's avatar
Krzysztof Gogolewski committed
524 525
    go subst ty@(FunTy _ mult arg res)
      = ty { ft_mult = go subst mult, ft_arg = go subst arg, ft_res = go subst res }
Ningning Xie's avatar
Ningning Xie committed
526 527 528
    go subst (ForAllTy (Bndr tv vis) t)
      = let (subst', tv') = substVarBndrUsing go subst tv in
        ForAllTy (Bndr tv' vis) (go subst' t)
529 530 531
    go subst (CastTy ty co)  = mkCastTy (go subst ty) (go_co subst co)
    go subst (CoercionTy co) = mkCoercionTy (go_co subst co)

Ningning Xie's avatar
Ningning Xie committed
532 533 534 535 536 537 538
    go_mco _     MRefl    = MRefl
    go_mco subst (MCo co) = MCo (go_co subst co)

    go_co subst (Refl ty)
      = mkNomReflCo (go subst ty)
    go_co subst (GRefl r ty mco)
      = mkGReflCo r (go subst ty) (go_mco subst mco)
539 540 541 542 543 544 545 546
       -- NB: coercions are always expanded upon creation
    go_co subst (TyConAppCo r tc args)
      = mkTyConAppCo r tc (map (go_co subst) args)
    go_co subst (AppCo co arg)
      = mkAppCo (go_co subst co) (go_co subst arg)
    go_co subst (ForAllCo tv kind_co co)
      = let (subst', tv', kind_co') = go_cobndr subst tv kind_co in
        mkForAllCo tv' kind_co' (go_co subst' co)
Krzysztof Gogolewski's avatar
Krzysztof Gogolewski committed
547 548
    go_co subst (FunCo r w co1 co2)
      = mkFunCo r (go_co subst w) (go_co subst co1) (go_co subst co2)
549 550 551 552 553 554 555 556 557 558
    go_co subst (CoVarCo cv)
      = substCoVar subst cv
    go_co subst (AxiomInstCo ax ind args)
      = mkAxiomInstCo ax ind (map (go_co subst) args)
    go_co subst (UnivCo p r t1 t2)
      = mkUnivCo (go_prov subst p) r (go subst t1) (go subst t2)
    go_co subst (SymCo co)
      = mkSymCo (go_co subst co)
    go_co subst (TransCo co1 co2)
      = mkTransCo (go_co subst co1) (go_co subst co2)
559 560
    go_co subst (NthCo r n co)
      = mkNthCo r n (go_co subst co)
561 562 563 564 565 566 567 568
    go_co subst (LRCo lr co)
      = mkLRCo lr (go_co subst co)
    go_co subst (InstCo co arg)
      = mkInstCo (go_co subst co) (go_co subst arg)
    go_co subst (KindCo co)
      = mkKindCo (go_co subst co)
    go_co subst (SubCo co)
      = mkSubCo (go_co subst co)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
569 570 571 572
    go_co subst (AxiomRuleCo ax cs)
      = AxiomRuleCo ax (map (go_co subst) cs)
    go_co _ (HoleCo h)
      = pprPanic "expandTypeSynonyms hit a hole" (ppr h)
573 574 575 576 577 578

    go_prov subst (PhantomProv co)    = PhantomProv (go_co subst co)
    go_prov subst (ProofIrrelProv co) = ProofIrrelProv (go_co subst co)
    go_prov _     p@(PluginProv _)    = p

      -- the "False" and "const" are to accommodate the type of
Simon Peyton Jones's avatar
Simon Peyton Jones committed
579
      -- substForAllCoBndrUsing, which is general enough to
580 581
      -- handle coercion optimization (which sometimes swaps the
      -- order of a coercion)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
582
    go_cobndr subst = substForAllCoBndrUsing False (go_co subst) subst
583

584 585 586 587 588 589 590 591 592 593 594 595 596 597 598

-- | Extract the RuntimeRep classifier of a type from its kind. For example,
-- @kindRep * = LiftedRep@; Panics if this is not possible.
-- Treats * and Constraint as the same
kindRep :: HasDebugCallStack => Kind -> Type
kindRep k = case kindRep_maybe k of
              Just r  -> r
              Nothing -> pprPanic "kindRep" (ppr k)

-- | Given a kind (TYPE rr), extract its RuntimeRep classifier rr.
-- For example, @kindRep_maybe * = Just LiftedRep@
-- Returns 'Nothing' if the kind is not of form (TYPE rr)
-- Treats * and Constraint as the same
kindRep_maybe :: HasDebugCallStack => Kind -> Maybe Type
kindRep_maybe kind
599
  | TyConApp tc [arg] <- coreFullView kind
600 601 602 603 604 605 606 607 608 609 610 611
  , tc `hasKey` tYPETyConKey    = Just arg
  | otherwise                   = Nothing

-- | This version considers Constraint to be the same as *. Returns True
-- if the argument is equivalent to Type/Constraint and False otherwise.
-- See Note [Kind Constraint and kind Type]
isLiftedTypeKind :: Kind -> Bool
isLiftedTypeKind kind
  = case kindRep_maybe kind of
      Just rep -> isLiftedRuntimeRep rep
      Nothing  -> False

612 613 614
pickyIsLiftedTypeKind :: Kind -> Bool
-- Checks whether the kind is literally
--      TYPE LiftedRep
Andrew Martin's avatar
Andrew Martin committed
615
-- or   TYPE ('BoxedRep 'Lifted)
616 617 618 619 620 621 622 623
-- or   Type
-- without expanding type synonyms or anything
-- Used only when deciding whether to suppress the ":: *" in
-- (a :: *) when printing kinded type variables
-- See Note [Suppressing * kinds] in GHC.Core.TyCo.Ppr
pickyIsLiftedTypeKind kind
  | TyConApp tc [arg] <- kind
  , tc `hasKey` tYPETyConKey
Andrew Martin's avatar
Andrew Martin committed
624 625 626 627 628 629 630
  , TyConApp rr_tc rr_args <- arg = case rr_args of
      [] -> rr_tc `hasKey` liftedRepTyConKey
      [rr_arg]
        | rr_tc `hasKey` boxedRepDataConKey
        , TyConApp lev [] <- rr_arg
        , lev `hasKey` liftedDataConKey -> True
      _ -> False
631 632 633 634
  | TyConApp tc [] <- kind
  , tc `hasKey` liftedTypeKindTyConKey = True
  | otherwise                          = False

635 636 637 638 639
isLiftedRuntimeRep :: Type -> Bool
-- isLiftedRuntimeRep is true of LiftedRep :: RuntimeRep
-- False of type variables (a :: RuntimeRep)
--   and of other reps e.g. (IntRep :: RuntimeRep)
isLiftedRuntimeRep rep
Andrew Martin's avatar
Andrew Martin committed
640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660
  | TyConApp rr_tc rr_args <- coreFullView rep
  , rr_tc `hasKey` boxedRepDataConKey
  = case rr_args of
      [rr_arg] -> isLiftedLevity rr_arg
      _ -> ASSERT( False ) True -- this should probably just panic
  | otherwise                          = False

isLiftedLevity :: Type -> Bool
isLiftedLevity lev
  | Just lev' <- coreView lev          = isLiftedLevity lev'
  | TyConApp lev_tc lev_args <- lev
  , lev_tc `hasKey` liftedDataConKey
  = ASSERT( null lev_args ) True
  | otherwise                          = False

isUnliftedLevity :: Type -> Bool
isUnliftedLevity lev
  | Just lev' <- coreView lev          = isUnliftedLevity lev'
  | TyConApp lev_tc lev_args <- lev
  , lev_tc `hasKey` unliftedDataConKey
  = ASSERT( null lev_args ) True
661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676
  | otherwise                          = False

-- | Returns True if the kind classifies unlifted types and False otherwise.
-- Note that this returns False for levity-polymorphic kinds, which may
-- be specialized to a kind that classifies unlifted types.
isUnliftedTypeKind :: Kind -> Bool
isUnliftedTypeKind kind
  = case kindRep_maybe kind of
      Just rep -> isUnliftedRuntimeRep rep
      Nothing  -> False

isUnliftedRuntimeRep :: Type -> Bool
-- True of definitely-unlifted RuntimeReps
-- False of           (LiftedRep :: RuntimeRep)
--   and of variables (a :: RuntimeRep)
isUnliftedRuntimeRep rep
Andrew Martin's avatar
Andrew Martin committed
677 678 679 680 681 682 683 684 685
  | TyConApp rr_tc args <- coreFullView rep   -- NB: args might be non-empty
                                              --     e.g. TupleRep [r1, .., rn]
  , isPromotedDataCon rr_tc =
      -- NB: args might be non-empty e.g. TupleRep [r1, .., rn]
      if (rr_tc `hasKey` boxedRepDataConKey)
        then case args of
          [TyConApp lev_tc []] -> lev_tc `hasKey` unliftedDataConKey
          _ -> False
        else True
686 687 688 689 690 691 692 693
        -- Avoid searching all the unlifted RuntimeRep type cons
        -- In the RuntimeRep data type, only LiftedRep is lifted
        -- But be careful of type families (F tys) :: RuntimeRep
  | otherwise {- Variables, applications -}
  = False

-- | Is this the type 'RuntimeRep'?
isRuntimeRepTy :: Type -> Bool
694 695 696 697 698
isRuntimeRepTy ty
  | TyConApp tc args <- coreFullView ty
  , tc `hasKey` runtimeRepTyConKey = ASSERT( null args ) True

  | otherwise = False
699 700 701 702 703

-- | Is a tyvar of type 'RuntimeRep'?
isRuntimeRepVar :: TyVar -> Bool
isRuntimeRepVar = isRuntimeRepTy . tyVarKind

Krzysztof Gogolewski's avatar
Krzysztof Gogolewski committed
704 705
-- | Is this the type 'Multiplicity'?
isMultiplicityTy :: Type -> Bool
706 707 708
isMultiplicityTy ty
  | TyConApp tc [] <- coreFullView ty = tc `hasKey` multiplicityTyConKey
  | otherwise                         = False
Krzysztof Gogolewski's avatar
Krzysztof Gogolewski committed
709 710 711 712 713

-- | Is a tyvar of type 'Multiplicity'?
isMultiplicityVar :: TyVar -> Bool
isMultiplicityVar = isMultiplicityTy . tyVarKind

714
{- *********************************************************************
715
*                                                                      *
716
               mapType
717 718 719 720 721 722
*                                                                      *
************************************************************************

These functions do a map-like operation over types, performing some operation
on all variables and binding sites. Primarily used for zonking.

723
Note [Efficiency for ForAllCo case of mapTyCoX]
724
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Sylvain Henry's avatar
Sylvain Henry committed
725
As noted in Note [Forall coercions] in GHC.Core.TyCo.Rep, a ForAllCo is a bit redundant.
Ningning Xie's avatar
Ningning Xie committed
726
It stores a TyCoVar and a Coercion, where the kind of the TyCoVar always matches
727 728 729
the left-hand kind of the coercion. This is convenient lots of the time, but
not when mapping a function over a coercion.

Ningning Xie's avatar
Ningning Xie committed
730
The problem is that tcm_tybinder will affect the TyCoVar's kind and
731 732 733 734 735 736 737 738 739 740 741 742 743 744
mapCoercion will affect the Coercion, and we hope that the results will be
the same. Even if they are the same (which should generally happen with
correct algorithms), then there is an efficiency issue. In particular,
this problem seems to make what should be a linear algorithm into a potentially
exponential one. But it's only going to be bad in the case where there's
lots of foralls in the kinds of other foralls. Like this:

  forall a : (forall b : (forall c : ...). ...). ...

This construction seems unlikely. So we'll do the inefficient, easy way
for now.

Note [Specialising mappers]
~~~~~~~~~~~~~~~~~~~~~~~~~~~
745
These INLINE pragmas are indispensable. mapTyCo and mapTyCoX are used
746
to implement zonking, and it's vital that they get specialised to the TcM
747
monad and the particular mapper in use.
748

749 750 751
Even specialising to the monad alone made a 20% allocation difference
in perf/compiler/T5030.

752
See Note [Specialising foldType] in "GHC.Core.TyCo.Rep" for more details of this
753
idiom.
754 755 756 757 758
-}

-- | This describes how a "map" operation over a type/coercion should behave
data TyCoMapper env m
  = TyCoMapper
759
      { tcm_tyvar :: env -> TyVar -> m Type
760
      , tcm_covar :: env -> CoVar -> m Coercion
Simon Peyton Jones's avatar
Simon Peyton Jones committed
761 762
      , tcm_hole  :: env -> CoercionHole -> m Coercion
          -- ^ What to do with coercion holes.
763
          -- See Note [Coercion holes] in "GHC.Core.TyCo.Rep".
764

Ningning Xie's avatar
Ningning Xie committed
765
      , tcm_tycobinder :: env -> TyCoVar -> ArgFlag -> m (env, TyCoVar)
766
          -- ^ The returned env is used in the extended scope
767 768

      , tcm_tycon :: TyCon -> m TyCon
Simon Peyton Jones's avatar
Simon Peyton Jones committed
769 770 771 772
          -- ^ This is used only for TcTyCons
          -- a) To zonk TcTyCons
          -- b) To turn TcTyCons into TyCons.
          --    See Note [Type checking recursive type and class declarations]
773
          --    in "GHC.Tc.TyCl"
774 775
      }

776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798
{-# INLINE mapTyCo #-}  -- See Note [Specialising mappers]
mapTyCo :: Monad m => TyCoMapper () m
         -> ( Type       -> m Type
            , [Type]     -> m [Type]
            , Coercion   -> m Coercion
            , [Coercion] -> m[Coercion])
mapTyCo mapper
  = case mapTyCoX mapper of
     (go_ty, go_tys, go_co, go_cos)
        -> (go_ty (), go_tys (), go_co (), go_cos ())

{-# INLINE mapTyCoX #-}  -- See Note [Specialising mappers]
mapTyCoX :: Monad m => TyCoMapper env m
         -> ( env -> Type       -> m Type
            , env -> [Type]     -> m [Type]
            , env -> Coercion   -> m Coercion
            , env -> [Coercion] -> m[Coercion])
mapTyCoX (TyCoMapper { tcm_tyvar = tyvar
                     , tcm_tycobinder = tycobinder
                     , tcm_tycon = tycon
                     , tcm_covar = covar
                     , tcm_hole = cohole })
  = (go_ty, go_tys, go_co, go_cos)
799
  where
800 801 802 803 804 805 806 807 808
    go_tys _   []       = return []
    go_tys env (ty:tys) = (:) <$> go_ty env ty <*> go_tys env tys

    go_ty env (TyVarTy tv)    = tyvar env tv
    go_ty env (AppTy t1 t2)   = mkAppTy <$> go_ty env t1 <*> go_ty env t2
    go_ty _   ty@(LitTy {})   = return ty
    go_ty env (CastTy ty co)  = mkCastTy <$> go_ty env ty <*> go_co env co
    go_ty env (CoercionTy co) = CoercionTy <$> go_co env co

Krzysztof Gogolewski's avatar
Krzysztof Gogolewski committed
809 810 811
    go_ty env ty@(FunTy _ w arg res)
      = do { w' <- go_ty env w; arg' <- go_ty env arg; res' <- go_ty env res
           ; return (ty { ft_mult = w', ft_arg = arg', ft_res = res' }) }
Simon Peyton Jones's avatar
Simon Peyton Jones committed
812

813
    go_ty env ty@(TyConApp tc tys)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
814
      | isTcTyCon tc
815
      = do { tc' <- tycon tc
816
           ; mkTyConApp tc' <$> go_tys env tys }
Simon Peyton Jones's avatar
Simon Peyton Jones committed
817 818 819 820 821 822

      -- Not a TcTyCon
      | null tys    -- Avoid allocation in this very
      = return ty   -- common case (E.g. Int, LiftedRep etc)

      | otherwise
823
      = mkTyConApp tc <$> go_tys env tys
Simon Peyton Jones's avatar
Simon Peyton Jones committed
824

825
    go_ty env (ForAllTy (Bndr tv vis) inner)
Ningning Xie's avatar
Ningning Xie committed
826
      = do { (env', tv') <- tycobinder env tv vis
827
           ; inner' <- go_ty env' inner
Ningning Xie's avatar
Ningning Xie committed
828
           ; return $ ForAllTy (Bndr tv' vis) inner' }
829

830 831 832 833 834 835 836 837 838
    go_cos _   []       = return []
    go_cos env (co:cos) = (:) <$> go_co env co <*> go_cos env cos

    go_mco _   MRefl    = return MRefl
    go_mco env (MCo co) = MCo <$> (go_co env co)

    go_co env (Refl ty)           = Refl <$> go_ty env ty
    go_co env (GRefl r ty mco)    = mkGReflCo r <$> go_ty env ty <*> go_mco env mco
    go_co env (AppCo c1 c2)       = mkAppCo <$> go_co env c1 <*> go_co env c2
Krzysztof Gogolewski's avatar
Krzysztof Gogolewski committed
839
    go_co env (FunCo r cw c1 c2)   = mkFunCo r <$> go_co env cw <*> go_co env c1 <*> go_co env c2
840 841 842 843 844 845 846 847 848 849 850 851 852 853 854 855 856 857 858 859 860 861 862 863 864 865
    go_co env (CoVarCo cv)        = covar env cv
    go_co env (HoleCo hole)       = cohole env hole
    go_co env (UnivCo p r t1 t2)  = mkUnivCo <$> go_prov env p <*> pure r
                                    <*> go_ty env t1 <*> go_ty env t2
    go_co env (SymCo co)          = mkSymCo <$> go_co env co
    go_co env (TransCo c1 c2)     = mkTransCo <$> go_co env c1 <*> go_co env c2
    go_co env (AxiomRuleCo r cos) = AxiomRuleCo r <$> go_cos env cos
    go_co env (NthCo r i co)      = mkNthCo r i <$> go_co env co
    go_co env (LRCo lr co)        = mkLRCo lr <$> go_co env co
    go_co env (InstCo co arg)     = mkInstCo <$> go_co env co <*> go_co env arg
    go_co env (KindCo co)         = mkKindCo <$> go_co env co
    go_co env (SubCo co)          = mkSubCo <$> go_co env co
    go_co env (AxiomInstCo ax i cos) = mkAxiomInstCo ax i <$> go_cos env cos
    go_co env co@(TyConAppCo r tc cos)
      | isTcTyCon tc
      = do { tc' <- tycon tc
           ; mkTyConAppCo r tc' <$> go_cos env cos }

      -- Not a TcTyCon
      | null cos    -- Avoid allocation in this very
      = return co   -- common case (E.g. Int, LiftedRep etc)

      | otherwise
      = mkTyConAppCo r tc <$> go_cos env cos
    go_co env (ForAllCo tv kind_co co)
      = do { kind_co' <- go_co env kind_co
Ningning Xie's avatar
Ningning Xie committed
866
           ; (env', tv') <- tycobinder env tv Inferred
867
           ; co' <- go_co env' co
868
           ; return $ mkForAllCo tv' kind_co' co' }
869 870 871 872 873
        -- See Note [Efficiency for ForAllCo case of mapTyCoX]

    go_prov env (PhantomProv co)    = PhantomProv <$> go_co env co
    go_prov env (ProofIrrelProv co) = ProofIrrelProv <$> go_co env co
    go_prov _   p@(PluginProv _)    = return p
874

875

876 877 878
{-
************************************************************************
*                                                                      *
879
\subsection{Constructor-specific functions}
880 881
*                                                                      *
************************************************************************