Type.hs 107 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

Richard Eisenberg's avatar
Richard Eisenberg committed
6
{-# LANGUAGE CPP, FlexibleContexts #-}
7
{-# OPTIONS_GHC -fno-warn-orphans #-}
Ian Lynagh's avatar
Ian Lynagh committed
8

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

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

batterseapower's avatar
batterseapower committed
16
        -- $representation_types
17
        TyThing(..), Type, ArgFlag(..), KindOrType, PredType, ThetaType,
Simon Peyton Jones's avatar
Simon Peyton Jones committed
18
        Var, TyVar, isTyVar, TyCoVar, TyBinder, TyVarBinder,
19
        KnotTied,
20

batterseapower's avatar
batterseapower committed
21
        -- ** Constructing and deconstructing types
22 23
        mkTyVarTy, mkTyVarTys, getTyVar, getTyVar_maybe, repGetTyVar_maybe,
        getCastedTyVar_maybe, tyVarKind,
24

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
25
        mkAppTy, mkAppTys, splitAppTy, splitAppTys, repSplitAppTys,
26
        splitAppTy_maybe, repSplitAppTy_maybe, tcRepSplitAppTy_maybe,
27

ian@well-typed.com's avatar
ian@well-typed.com committed
28
        mkFunTy, mkFunTys, splitFunTy, splitFunTy_maybe,
29
        splitFunTys, funResultTy, funArgTy,
30

ian@well-typed.com's avatar
ian@well-typed.com committed
31
        mkTyConApp, mkTyConTy,
32 33
        tyConAppTyCon_maybe, tyConAppTyConPicky_maybe,
        tyConAppArgs_maybe, tyConAppTyCon, tyConAppArgs,
34
        splitTyConApp_maybe, splitTyConApp, tyConAppArgN, nextRole,
Ben Gamari's avatar
Ben Gamari committed
35
        tcRepSplitTyConApp_maybe, tcSplitTyConApp_maybe,
36 37 38
        splitListTyConApp_maybe,
        repSplitTyConApp_maybe,

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
39
        mkForAllTy, mkForAllTys, mkInvForAllTys, mkSpecForAllTys,
Simon Peyton Jones's avatar
Simon Peyton Jones committed
40 41 42 43
        mkVisForAllTys, mkInvForAllTy,
        splitForAllTys, splitForAllTyVarBndrs,
        splitForAllTy_maybe, splitForAllTy,
        splitPiTy_maybe, splitPiTy, splitPiTys,
44
        mkPiTy, mkPiTys, mkTyConBindersPreferAnon,
Simon Peyton Jones's avatar
Simon Peyton Jones committed
45
        mkLamType, mkLamTypes,
46
        piResultTy, piResultTys,
47
        applyTysX, dropForAlls,
48

49 50
        mkNumLitTy, isNumLitTy,
        mkStrLitTy, isStrLitTy,
51
        isLitTy,
52

Ben Gamari's avatar
Ben Gamari committed
53 54
        getRuntimeRep_maybe, getRuntimeRepFromKind_maybe,

Simon Peyton Jones's avatar
Simon Peyton Jones committed
55
        mkCastTy, mkCoercionTy, splitCastTy_maybe,
56

57
        userTypeError_maybe, pprUserTypeErrorTy,
58

59
        coAxNthLHS,
60 61 62
        stripCoercionTy, splitCoercionType_maybe,

        splitPiTysInvisible, filterOutInvisibleTypes,
63
        partitionInvisibles,
64 65
        synTyConResKind,

lukemaurer's avatar
lukemaurer committed
66 67
        modifyJoinResTy, setJoinResTy,

68 69
        -- Analyzing types
        TyCoMapper(..), mapType, mapCoercion,
ian@well-typed.com's avatar
ian@well-typed.com committed
70 71 72 73 74

        -- (Newtypes)
        newTyConInstRhs,

        -- Pred types
batterseapower's avatar
batterseapower committed
75
        mkFamilyTyConApp,
ian@well-typed.com's avatar
ian@well-typed.com committed
76
        isDictLikeTy,
77 78 79
        mkPrimEqPred, mkReprPrimEqPred, mkPrimEqPredRole,
        equalityTyCon,
        mkHeteroPrimEqPred, mkHeteroReprPrimEqPred,
80
        mkClassPred,
81
        isClassPred, isEqPred, isNomEqPred,
82
        isIPPred, isIPPred_maybe, isIPTyCon, isIPClass,
83
        isCTupleClass,
ian@well-typed.com's avatar
ian@well-typed.com committed
84

batterseapower's avatar
batterseapower committed
85
        -- Deconstructing predicate types
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
86
        PredTree(..), EqRel(..), eqRelRole, classifyPredType,
batterseapower's avatar
batterseapower committed
87
        getClassPredTys, getClassPredTys_maybe,
Joachim Breitner's avatar
Joachim Breitner committed
88
        getEqPredTys, getEqPredTys_maybe, getEqPredRole,
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
89
        predTypeEqRel,
90

91
        -- ** Binders
92
        sameVis,
Simon Peyton Jones's avatar
Simon Peyton Jones committed
93
        mkTyVarBinder, mkTyVarBinders,
94
        mkAnonBinder,
Simon Peyton Jones's avatar
Simon Peyton Jones committed
95
        isAnonTyBinder, isNamedTyBinder,
96
        binderVar, binderVars, binderKind, binderArgFlag,
97
        tyBinderType, tyBinderVar_maybe,
Simon Peyton Jones's avatar
Simon Peyton Jones committed
98
        binderRelevantType_maybe, caseBinder,
99
        isVisibleArgFlag, isInvisibleArgFlag, isVisibleBinder, isInvisibleBinder,
100
        tyConBindersTyBinders,
101

ian@well-typed.com's avatar
ian@well-typed.com committed
102
        -- ** Common type constructors
batterseapower's avatar
batterseapower committed
103
        funTyCon,
104

batterseapower's avatar
batterseapower committed
105
        -- ** Predicates on types
106
        isTyVarTy, isFunTy, isDictTy, isPredTy, isCoercionTy,
107
        isCoercionTy_maybe, isCoercionType, isForAllTy,
108
        isPiTy, isTauTy, isFamFreeTy,
batterseapower's avatar
batterseapower committed
109

lukemaurer's avatar
lukemaurer committed
110 111
        isValidJoinPointType,

ian@well-typed.com's avatar
ian@well-typed.com committed
112
        -- (Lifting and boxity)
Richard Eisenberg's avatar
Richard Eisenberg committed
113
        isLiftedType_maybe, isUnliftedType, isUnboxedTupleType, isUnboxedSumType,
114
        isAlgType, isDataFamilyAppType,
ian@well-typed.com's avatar
ian@well-typed.com committed
115
        isPrimitiveType, isStrictType,
116 117 118
        isRuntimeRepTy, isRuntimeRepVar, isRuntimeRepKindedTy,
        dropRuntimeRepArgs,
        getRuntimeRep, getRuntimeRepFromKind,
119

ian@well-typed.com's avatar
ian@well-typed.com committed
120
        -- * Main data types representing Kinds
121
        Kind,
batterseapower's avatar
batterseapower committed
122 123

        -- ** Finding the kind of a type
Richard Eisenberg's avatar
Richard Eisenberg committed
124
        typeKind, isTypeLevPoly, resultIsLevPoly,
125
        tcIsLiftedTypeKind, tcIsConstraintKind, tcReturnsConstraintKind,
ian@well-typed.com's avatar
ian@well-typed.com committed
126

127
        -- ** Common Kind
128
        liftedTypeKind,
batterseapower's avatar
batterseapower committed
129

ian@well-typed.com's avatar
ian@well-typed.com committed
130
        -- * Type free variables
Simon Peyton Jones's avatar
Simon Peyton Jones committed
131 132
        tyCoFVsOfType, tyCoFVsBndr,
        tyCoVarsOfType, tyCoVarsOfTypes,
133 134
        tyCoVarsOfTypeDSet,
        coVarsOfType,
135
        coVarsOfTypes, closeOverKinds, closeOverKindsList,
Richard Eisenberg's avatar
Richard Eisenberg committed
136
        noFreeVarsOfType,
137
        splitVisVarsOfType, splitVisVarsOfTypes,
ian@well-typed.com's avatar
ian@well-typed.com committed
138
        expandTypeSynonyms,
139
        typeSize, occCheckExpand,
140 141

        -- * Well-scoped lists of variables
142
        dVarSetElemsWellScoped, toposortTyVars, tyCoVarsOfTypeWellScoped,
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
143
        tyCoVarsOfTypesWellScoped,
144

ian@well-typed.com's avatar
ian@well-typed.com committed
145
        -- * Type comparison
niteria's avatar
niteria committed
146 147
        eqType, eqTypeX, eqTypes, nonDetCmpType, nonDetCmpTypes, nonDetCmpTypeX,
        nonDetCmpTypesX, nonDetCmpTc,
148
        eqVarBndrs,
149

ian@well-typed.com's avatar
ian@well-typed.com committed
150
        -- * Forcing evaluation of types
batterseapower's avatar
batterseapower committed
151
        seqType, seqTypes,
152

batterseapower's avatar
batterseapower committed
153
        -- * Other views onto Types
Ben Gamari's avatar
Ben Gamari committed
154
        coreView, tcView,
batterseapower's avatar
batterseapower committed
155

156
        tyConsOfType,
batterseapower's avatar
batterseapower committed
157

ian@well-typed.com's avatar
ian@well-typed.com committed
158 159
        -- * Main type substitution data types
        TvSubstEnv,     -- Representation widely visible
160
        TCvSubst(..),    -- Representation visible to a few friends
ian@well-typed.com's avatar
ian@well-typed.com committed
161 162

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

niteria's avatar
niteria committed
165
        mkTCvSubst, zipTvSubst, mkTvSubstPrs,
166
        notElemTCvSubst,
167
        getTvSubstEnv, setTvSubstEnv,
168
        zapTCvSubst, getTCvInScope, getTCvSubstRangeFVs,
169
        extendTCvInScope, extendTCvInScopeList, extendTCvInScopeSet,
170
        extendTCvSubst, extendCvSubst,
Richard Eisenberg's avatar
Richard Eisenberg committed
171
        extendTvSubst, extendTvSubstBinderAndInScope,
172
        extendTvSubstList, extendTvSubstAndInScope,
173
        extendTvSubstWithClone,
174 175
        isInScope, composeTCvSubstEnv, composeTCvSubst, zipTyEnv, zipCoEnv,
        isEmptyTCvSubst, unionTCvSubst,
176

ian@well-typed.com's avatar
ian@well-typed.com committed
177 178
        -- ** Performing substitution on types and kinds
        substTy, substTys, substTyWith, substTysWith, substTheta,
179 180
        substTyAddInScope,
        substTyUnchecked, substTysUnchecked, substThetaUnchecked,
181
        substTyWithUnchecked,
182
        substCoUnchecked, substCoWithUnchecked,
Simon Peyton Jones's avatar
Simon Peyton Jones committed
183
        substTyVarBndr, substTyVarBndrs, substTyVar, substTyVars,
184
        cloneTyVarBndr, cloneTyVarBndrs, lookupTyVar,
185

ian@well-typed.com's avatar
ian@well-typed.com committed
186
        -- * Pretty-printing
187 188
        pprType, pprParendType, pprPrecType,
        pprTypeApp, pprTyThingCategory, pprShortTyThing,
Ben Gamari's avatar
Ben Gamari committed
189
        pprTvBndr, pprTvBndrs, pprForAll, pprUserForAll,
190
        pprSigmaType, ppSuggestExplicitKinds,
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
191
        pprTheta, pprThetaArrowTy, pprClassPred,
dreixel's avatar
dreixel committed
192
        pprKind, pprParendKind, pprSourceTyCon,
193
        PprPrec(..), topPrec, sigPrec, opPrec, funPrec, appPrec, maybeParen,
194
        pprTyVar, pprTyVars,
195
        pprWithTYPE,
Simon Peyton Jones's avatar
Simon Peyton Jones committed
196 197 198 199 200

        -- * Tidying type related things up for printing
        tidyType,      tidyTypes,
        tidyOpenType,  tidyOpenTypes,
        tidyOpenKind,
201 202
        tidyTyCoVarBndr, tidyTyCoVarBndrs, tidyFreeTyCoVars,
        tidyOpenTyCoVar, tidyOpenTyCoVars,
Simon Peyton Jones's avatar
Simon Peyton Jones committed
203 204
        tidyTyVarOcc,
        tidyTopType,
205
        tidyKind,
Simon Peyton Jones's avatar
Simon Peyton Jones committed
206
        tidyTyVarBinder, tidyTyVarBinders
207
    ) where
208

209 210
#include "HsVersions.h"

211 212
import GhcPrelude

lukemaurer's avatar
lukemaurer committed
213 214
import BasicTypes

215
-- We import the representation and primitive functions from TyCoRep.
216 217
-- Many things are reexported, but not the representation!

dreixel's avatar
dreixel committed
218
import Kind
219
import TyCoRep
220

221
-- friends:
222
import Var
223 224
import VarEnv
import VarSet
David Feuer's avatar
David Feuer committed
225
import UniqSet
226

227 228
import Class
import TyCon
229
import TysPrim
230 231 232
import {-# SOURCE #-} TysWiredIn ( listTyCon, typeNatKind
                                 , typeSymbolKind, liftedTypeKind )
import PrelNames
233
import CoAxiom
234 235 236 237 238 239 240
import {-# SOURCE #-} Coercion( mkNomReflCo, mkGReflCo, mkReflCo
                              , mkTyConAppCo, mkAppCo, mkCoVarCo, mkAxiomRuleCo
                              , mkForAllCo, mkFunCo, mkAxiomInstCo, mkUnivCo
                              , mkSymCo, mkTransCo, mkNthCo, mkLRCo, mkInstCo
                              , mkKindCo, mkSubCo, mkFunCo, mkAxiomInstCo
                              , decomposePiCos, coercionKind, coercionType
                              , isReflexiveCo, seqCo )
241

242
-- others
243
import Util
244
import Outputable
245
import FastString
246
import Pair
247
import DynFlags  ( gopt_set, GeneralFlag(Opt_PrintExplicitRuntimeReps) )
248 249
import ListSetOps
import Digraph
250
import Unique ( nonDetCmpUnique )
simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
251

ian@well-typed.com's avatar
ian@well-typed.com committed
252
import Maybes           ( orElse )
253
import Data.Maybe       ( isJust, mapMaybe )
254
import Control.Monad    ( guard )
255
import Control.Arrow    ( first, second )
256

batterseapower's avatar
batterseapower committed
257 258
-- $type_classification
-- #type_classification#
ian@well-typed.com's avatar
ian@well-typed.com committed
259
--
batterseapower's avatar
batterseapower committed
260
-- Types are one of:
ian@well-typed.com's avatar
ian@well-typed.com committed
261
--
batterseapower's avatar
batterseapower committed
262
-- [Unboxed]            Iff its representation is other than a pointer
ian@well-typed.com's avatar
ian@well-typed.com committed
263 264
--                      Unboxed types are also unlifted.
--
batterseapower's avatar
batterseapower committed
265
-- [Lifted]             Iff it has bottom as an element.
ian@well-typed.com's avatar
ian@well-typed.com committed
266 267 268 269 270 271
--                      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
272
-- [Algebraic]          Iff it is a type with one or more constructors, whether
ian@well-typed.com's avatar
ian@well-typed.com committed
273 274 275 276 277 278
--                      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
279
-- [Data]               Iff it is a type declared with @data@, or a boxed tuple.
ian@well-typed.com's avatar
ian@well-typed.com committed
280
--
batterseapower's avatar
batterseapower committed
281
-- [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
282
--
batterseapower's avatar
batterseapower committed
283 284
-- 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
285
--
batterseapower's avatar
batterseapower committed
286 287 288
-- 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
289
--
batterseapower's avatar
batterseapower committed
290
-- Some examples of type classifications that may make this a bit clearer are:
ian@well-typed.com's avatar
ian@well-typed.com committed
291
--
batterseapower's avatar
batterseapower committed
292
-- @
293
-- Type          primitive       boxed           lifted          algebraic
batterseapower's avatar
batterseapower committed
294
-- -----------------------------------------------------------------------------
295 296 297 298 299 300
-- 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
301 302 303 304 305
-- @

-- $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
306
-- passes and the rest of the back end is concerned.
batterseapower's avatar
batterseapower committed
307 308 309 310 311
--
-- 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
-- if they are spotted, to the best of it's abilities. If you don't want this
-- to happen, use the equivalent functions from the "TcType" module.
312

313 314 315
{-
************************************************************************
*                                                                      *
ian@well-typed.com's avatar
ian@well-typed.com committed
316
                Type representation
317 318
*                                                                      *
************************************************************************
Ben Gamari's avatar
Ben Gamari committed
319 320 321 322 323 324 325 326 327 328 329 330

Note [coreView vs tcView]
~~~~~~~~~~~~~~~~~~~~~~~~~
So far as the typechecker is concerned, 'Constraint' and 'TYPE LiftedRep' are distinct kinds.

But in Core these two are treated as identical.

We implement this by making 'coreView' convert 'Constraint' to 'TYPE LiftedRep' on the fly.
The function tcView (used in the type checker) does not do this.

See also Trac #11715, which tracks removing this inconsistency.

331
-}
332

Ben Gamari's avatar
Ben Gamari committed
333 334 335
-- | Gives the typechecker view of a type. This unwraps synonyms but
-- leaves 'Constraint' alone. c.f. coreView, which turns Constraint into
-- TYPE LiftedRep. Returns Nothing if no unwrapping happens.
336
-- See also Note [coreView vs tcView]
Ben Gamari's avatar
Ben Gamari committed
337 338 339 340 341 342 343 344 345 346 347
{-# INLINE tcView #-}
tcView :: Type -> Maybe Type
tcView (TyConApp tc tys) | Just (tenv, rhs, tys') <- expandSynTyCon_maybe tc tys
  = Just (mkAppTys (substTy (mkTvSubstPrs tenv) rhs) tys')
               -- The free vars of 'rhs' should all be bound by 'tenv', so it's
               -- ok to use 'substTy' here.
               -- See also Note [The substitution invariant] in TyCoRep.
               -- Its important to use mkAppTys, rather than (foldl AppTy),
               -- because the function part might well return a
               -- partially-applied type constructor; indeed, usually will!
tcView _ = Nothing
348

349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370
{-# INLINE coreView #-}
coreView :: Type -> Maybe Type
-- ^ This function Strips off the /top layer only/ of a type synonym
-- application (if any) its underlying representation type.
-- Returns Nothing if there is nothing to look through.
-- This function considers 'Constraint' to be a synonym of @TYPE LiftedRep@.
--
-- 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)
  | Just (tenv, rhs, tys') <- expandSynTyCon_maybe tc tys
  = Just (mkAppTys (substTy (mkTvSubstPrs tenv) rhs) tys')
    -- This equation is exactly like tcView

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

coreView _ = Nothing

371 372 373 374 375
-----------------------------------------------
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.
376 377 378
--
-- 'expandTypeSynonyms' only expands out type synonyms mentioned in the type,
-- not in the kinds of any TyCon or TyVar mentioned in the type.
379 380
--
-- Keep this synchronized with 'synonymTyConsOfType'
ian@well-typed.com's avatar
ian@well-typed.com committed
381
expandTypeSynonyms ty
382
  = go (mkEmptyTCvSubst in_scope) ty
383
  where
384 385
    in_scope = mkInScopeSet (tyCoVarsOfType ty)

386
    go subst (TyConApp tc tys)
387 388 389 390 391 392 393 394 395 396
      | 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
            -- (Trac #11665)
        in  mkAppTys (go subst' rhs) tys'
397
      | otherwise
398 399 400 401
      = TyConApp tc expanded_tys
      where
        expanded_tys = (map (go subst) tys)

402 403 404
    go _     (LitTy l)     = LitTy l
    go subst (TyVarTy tv)  = substTyVar subst tv
    go subst (AppTy t1 t2) = mkAppTy (go subst t1) (go subst t2)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
405
    go subst (FunTy arg res)
406
      = mkFunTy (go subst arg) (go subst res)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
407
    go subst (ForAllTy (TvBndr tv vis) t)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
408
      = let (subst', tv') = substTyVarBndrUsing go subst tv in
Simon Peyton Jones's avatar
Simon Peyton Jones committed
409
        ForAllTy (TvBndr tv' vis) (go subst' t)
410 411 412
    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
413 414 415 416 417 418 419
    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)
420 421 422 423 424 425 426 427
       -- 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)
Ben Gamari's avatar
Ben Gamari committed
428 429
    go_co subst (FunCo r co1 co2)
      = mkFunCo r (go_co subst co1) (go_co subst co2)
430 431 432 433 434 435 436 437 438 439
    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)
440 441
    go_co subst (NthCo r n co)
      = mkNthCo r n (go_co subst co)
442 443 444 445 446 447 448 449
    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
450 451 452 453
    go_co subst (AxiomRuleCo ax cs)
      = AxiomRuleCo ax (map (go_co subst) cs)
    go_co _ (HoleCo h)
      = pprPanic "expandTypeSynonyms hit a hole" (ppr h)
454 455 456 457 458 459 460

    go_prov _     UnsafeCoerceProv    = UnsafeCoerceProv
    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
461
      -- substForAllCoBndrUsing, which is general enough to
462 463
      -- handle coercion optimization (which sometimes swaps the
      -- order of a coercion)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
464
    go_cobndr subst = substForAllCoBndrUsing False (go_co subst) subst
465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509

{-
************************************************************************
*                                                                      *
   Analyzing types
*                                                                      *
************************************************************************

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

Note [Efficiency for mapCoercion ForAllCo case]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
As noted in Note [Forall coercions] in TyCoRep, a ForAllCo is a bit redundant.
It stores a TyVar and a Coercion, where the kind of the TyVar always matches
the left-hand kind of the coercion. This is convenient lots of the time, but
not when mapping a function over a coercion.

The problem is that tcm_tybinder will affect the TyVar's kind and
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]
~~~~~~~~~~~~~~~~~~~~~~~~~~~
These INLINABLE pragmas are indispensable. mapType/mapCoercion are used
to implement zonking, and it's vital that they get specialised to the TcM
monad. This specialisation happens automatically (that is, without a
SPECIALISE pragma) as long as the definitions are INLINABLE. For example,
this one change made a 20% allocation difference in perf/compiler/T5030.

-}

-- | This describes how a "map" operation over a type/coercion should behave
data TyCoMapper env m
  = TyCoMapper
      { tcm_smart :: Bool -- ^ Should the new type be created with smart
510
                          -- constructors?
511 512
      , tcm_tyvar :: env -> TyVar -> m Type
      , tcm_covar :: env -> CoVar -> m Coercion
Simon Peyton Jones's avatar
Simon Peyton Jones committed
513 514 515
      , tcm_hole  :: env -> CoercionHole -> m Coercion
          -- ^ What to do with coercion holes.
          -- See Note [Coercion holes] in TyCoRep.
516

517
      , tcm_tybinder :: env -> TyVar -> ArgFlag -> m (env, TyVar)
518
          -- ^ The returned env is used in the extended scope
519 520 521 522 523

      , tcm_tycon :: TyCon -> m TyCon
          -- ^ This is used only to turn 'TcTyCon's into 'TyCon's.
          -- See Note [Type checking recursive type and class declarations]
          -- in TcTyClsDecls
524 525 526
      }

{-# INLINABLE mapType #-}  -- See Note [Specialising mappers]
527
mapType :: Monad m => TyCoMapper env m -> env -> Type -> m Type
528
mapType mapper@(TyCoMapper { tcm_smart = smart, tcm_tyvar = tyvar
529
                           , tcm_tybinder = tybinder, tcm_tycon = tycon })
530 531 532 533 534
        env ty
  = go ty
  where
    go (TyVarTy tv) = tyvar env tv
    go (AppTy t1 t2) = mkappty <$> go t1 <*> go t2
535 536 537 538 539 540
    go t@(TyConApp tc []) | not (isTcTyCon tc)
                          = return t  -- avoid allocation in this exceedingly
                                      -- common case (mostly, for *)
    go (TyConApp tc tys)
      = do { tc' <- tycon tc
           ; mktyconapp tc' <$> mapM go tys }
Simon Peyton Jones's avatar
Simon Peyton Jones committed
541 542
    go (FunTy arg res)   = FunTy <$> go arg <*> go res
    go (ForAllTy (TvBndr tv vis) inner)
543 544
      = do { (env', tv') <- tybinder env tv vis
           ; inner' <- mapType mapper env' inner
Simon Peyton Jones's avatar
Simon Peyton Jones committed
545 546 547
           ; return $ ForAllTy (TvBndr tv' vis) inner' }
    go ty@(LitTy {})   = return ty
    go (CastTy ty co)  = mkcastty <$> go ty <*> mapCoercion mapper env co
548 549
    go (CoercionTy co) = CoercionTy <$> mapCoercion mapper env co

Simon Peyton Jones's avatar
Simon Peyton Jones committed
550 551 552
    (mktyconapp, mkappty, mkcastty)
      | smart     = (mkTyConApp, mkAppTy, mkCastTy)
      | otherwise = (TyConApp,   AppTy,   CastTy)
553 554

{-# INLINABLE mapCoercion #-}  -- See Note [Specialising mappers]
555
mapCoercion :: Monad m
556 557
            => TyCoMapper env m -> env -> Coercion -> m Coercion
mapCoercion mapper@(TyCoMapper { tcm_smart = smart, tcm_covar = covar
558 559
                               , tcm_hole = cohole, tcm_tybinder = tybinder
                               , tcm_tycon = tycon })
560 561 562
            env co
  = go co
  where
Ningning Xie's avatar
Ningning Xie committed
563 564 565 566 567
    go_mco MRefl    = return MRefl
    go_mco (MCo co) = MCo <$> (go co)

    go (Refl ty) = Refl <$> mapType mapper env ty
    go (GRefl r ty mco) = mkgreflco r <$> mapType mapper env ty <*> (go_mco mco)
568
    go (TyConAppCo r tc args)
569 570
      = do { tc' <- tycon tc
           ; mktyconappco r tc' <$> mapM go args }
571 572 573
    go (AppCo c1 c2) = mkappco <$> go c1 <*> go c2
    go (ForAllCo tv kind_co co)
      = do { kind_co' <- go kind_co
574
           ; (env', tv') <- tybinder env tv Inferred
575 576 577
           ; co' <- mapCoercion mapper env' co
           ; return $ mkforallco tv' kind_co' co' }
        -- See Note [Efficiency for mapCoercion ForAllCo case]
Ben Gamari's avatar
Ben Gamari committed
578
    go (FunCo r c1 c2) = mkFunCo r <$> go c1 <*> go c2
579 580 581
    go (CoVarCo cv) = covar env cv
    go (AxiomInstCo ax i args)
      = mkaxiominstco ax i <$> mapM go args
Simon Peyton Jones's avatar
Simon Peyton Jones committed
582
    go (HoleCo hole) = cohole env hole
583 584 585 586 587 588
    go (UnivCo p r t1 t2)
      = mkunivco <$> go_prov p <*> pure r
                 <*> mapType mapper env t1 <*> mapType mapper env t2
    go (SymCo co) = mksymco <$> go co
    go (TransCo c1 c2) = mktransco <$> go c1 <*> go c2
    go (AxiomRuleCo r cos) = AxiomRuleCo r <$> mapM go cos
589
    go (NthCo r i co)      = mknthco r i <$> go co
590 591 592 593 594 595 596 597 598 599 600
    go (LRCo lr co)        = mklrco lr <$> go co
    go (InstCo co arg)     = mkinstco <$> go co <*> go arg
    go (KindCo co)         = mkkindco <$> go co
    go (SubCo co)          = mksubco <$> go co

    go_prov UnsafeCoerceProv    = return UnsafeCoerceProv
    go_prov (PhantomProv co)    = PhantomProv <$> go co
    go_prov (ProofIrrelProv co) = ProofIrrelProv <$> go co
    go_prov p@(PluginProv _)    = return p

    ( mktyconappco, mkappco, mkaxiominstco, mkunivco
Ningning Xie's avatar
Ningning Xie committed
601 602
      , mksymco, mktransco, mknthco, mklrco, mkinstco
      , mkkindco, mksubco, mkforallco, mkgreflco)
603 604
      | smart
      = ( mkTyConAppCo, mkAppCo, mkAxiomInstCo, mkUnivCo
Ningning Xie's avatar
Ningning Xie committed
605 606
        , mkSymCo, mkTransCo, mkNthCo, mkLRCo, mkInstCo
        , mkKindCo, mkSubCo, mkForAllCo, mkGReflCo )
607 608
      | otherwise
      = ( TyConAppCo, AppCo, AxiomInstCo, UnivCo
Ningning Xie's avatar
Ningning Xie committed
609 610
        , SymCo, TransCo, NthCo, LRCo, InstCo
        , KindCo, SubCo, ForAllCo, GRefl )
611

612 613 614
{-
************************************************************************
*                                                                      *
615
\subsection{Constructor-specific functions}
616 617
*                                                                      *
************************************************************************
sof's avatar
sof committed
618 619


620
---------------------------------------------------------------------
ian@well-typed.com's avatar
ian@well-typed.com committed
621 622
                                TyVarTy
                                ~~~~~~~
623 624
-}

batterseapower's avatar
batterseapower committed
625 626
-- | Attempts to obtain the type variable underlying a 'Type', and panics with the
-- given message if this is not a type variable type. See also 'getTyVar_maybe'
627
getTyVar :: String -> Type -> TyVar
628
getTyVar msg ty = case getTyVar_maybe ty of
ian@well-typed.com's avatar
ian@well-typed.com committed
629 630
                    Just tv -> tv
                    Nothing -> panic ("getTyVar: " ++ msg)
631

632
isTyVarTy :: Type -> Bool
633 634
isTyVarTy ty = isJust (getTyVar_maybe ty)

batterseapower's avatar
batterseapower committed
635
-- | Attempts to obtain the type variable underlying a 'Type'
636
getTyVar_maybe :: Type -> Maybe TyVar
637
getTyVar_maybe ty | Just ty' <- coreView ty = getTyVar_maybe ty'
638 639 640
                  | otherwise               = repGetTyVar_maybe ty

-- | If the type is a tyvar, possibly under a cast, returns it, along
641 642
-- with the coercion. Thus, the co is :: kind tv ~N kind type
getCastedTyVar_maybe :: Type -> Maybe (TyVar, CoercionN)
643 644 645 646 647 648 649 650 651 652 653
getCastedTyVar_maybe ty | Just ty' <- coreView ty = getCastedTyVar_maybe ty'
getCastedTyVar_maybe (CastTy (TyVarTy tv) co)     = Just (tv, co)
getCastedTyVar_maybe (TyVarTy tv)
  = Just (tv, mkReflCo Nominal (tyVarKind tv))
getCastedTyVar_maybe _                            = Nothing

-- | Attempts to obtain the type variable underlying a 'Type', without
-- any expansion
repGetTyVar_maybe :: Type -> Maybe TyVar
repGetTyVar_maybe (TyVarTy tv) = Just tv
repGetTyVar_maybe _            = Nothing
654

655
{-
656
---------------------------------------------------------------------
ian@well-typed.com's avatar
ian@well-typed.com committed
657 658 659
                                AppTy
                                ~~~~~
We need to be pretty careful with AppTy to make sure we obey the
660 661
invariant that a TyConApp is always visibly so.  mkAppTy maintains the
invariant: use it.
662 663 664 665 666

Note [Decomposing fat arrow c=>t]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Can we unify (a b) with (Eq a => ty)?   If we do so, we end up with
a partial application like ((=>) Eq a) which doesn't make sense in
Gabor Greif's avatar
Gabor Greif committed
667
source Haskell.  In contrast, we *can* unify (a b) with (t1 -> t2).
668 669 670 671 672 673 674 675 676 677 678 679 680 681
Here's an example (Trac #9858) of how you might do it:
   i :: (Typeable a, Typeable b) => Proxy (a b) -> TypeRep
   i p = typeRep p

   j = i (Proxy :: Proxy (Eq Int => Int))
The type (Proxy (Eq Int => Int)) is only accepted with -XImpredicativeTypes,
but suppose we want that.  But then in the call to 'i', we end
up decomposing (Eq Int => Int), and we definitely don't want that.

This really only applies to the type checker; in Core, '=>' and '->'
are the same, as are 'Constraint' and '*'.  But for now I've put
the test in repSplitAppTy_maybe, which applies throughout, because
the other calls to splitAppTy are in Unify, which is also used by
the type checker (e.g. when matching type-function equations).
682

683
-}
684

batterseapower's avatar
batterseapower committed
685
-- | Applies a type to another, as in e.g. @k a@
686
mkAppTy :: Type -> Type -> Type
687 688
  -- See Note [Respecting definitional equality], invariant (EQ1).
mkAppTy (CastTy fun_ty co) arg_ty
689
  | ([arg_co], res_co) <- decomposePiCos co (coercionKind co) [arg_ty]
690 691
  = (fun_ty `mkAppTy` (arg_ty `mkCastTy` arg_co)) `mkCastTy` res_co

692 693
mkAppTy (TyConApp tc tys) ty2 = mkTyConApp tc (tys ++ [ty2])
mkAppTy ty1               ty2 = AppTy ty1 ty2
ian@well-typed.com's avatar
ian@well-typed.com committed
694 695 696 697 698 699 700 701
        -- Note that the TyConApp could be an
        -- under-saturated type synonym.  GHC allows that; e.g.
        --      type Foo k = k a -> k a
        --      type Id x = x
        --      foo :: Foo Id -> Foo Id
        --
        -- Here Id is partially applied in the type sig for Foo,
        -- but once the type synonyms are expanded all is well
702

703
mkAppTys :: Type -> [Type] -> Type
ian@well-typed.com's avatar
ian@well-typed.com committed
704
mkAppTys ty1                []   = ty1
705 706 707 708
mkAppTys (CastTy fun_ty co) arg_tys  -- much more efficient then nested mkAppTy
                                     -- Why do this? See (EQ1) of
                                     -- Note [Respecting definitional equality]
                                     -- in TyCoRep
709
  = foldl' AppTy ((mkAppTys fun_ty casted_arg_tys) `mkCastTy` res_co) leftovers
710
  where
711
    (arg_cos, res_co) = decomposePiCos co (coercionKind co) arg_tys
712 713
    (args_to_cast, leftovers) = splitAtList arg_cos arg_tys
    casted_arg_tys = zipWith mkCastTy args_to_cast arg_cos
714
mkAppTys (TyConApp tc tys1) tys2 = mkTyConApp tc (tys1 ++ tys2)
715
mkAppTys ty1                tys2 = foldl' AppTy ty1 tys2
716

717
-------------
718
splitAppTy_maybe :: Type -> Maybe (Type, Type)
batterseapower's avatar
batterseapower committed
719 720 721
-- ^ Attempt to take a type application apart, whether it is a
-- function, type constructor, or plain type application. Note
-- that type family applications are NEVER unsaturated by this!
722
splitAppTy_maybe ty | Just ty' <- coreView ty
ian@well-typed.com's avatar
ian@well-typed.com committed
723
                    = splitAppTy_maybe ty'
724
splitAppTy_maybe ty = repSplitAppTy_maybe ty
725

726
-------------
727
repSplitAppTy_maybe :: HasDebugCallStack => Type -> Maybe (Type,Type)
ian@well-typed.com's avatar
ian@well-typed.com committed
728
-- ^ Does the AppTy split as in 'splitAppTy_maybe', but assumes that
batterseapower's avatar
batterseapower committed
729
-- any Core view stuff is already done
Ben Gamari's avatar
Ben Gamari committed
730 731
repSplitAppTy_maybe (FunTy ty1 ty2)
  = Just (TyConApp funTyCon [rep1, rep2, ty1], ty2)
732 733 734
  where
    rep1 = getRuntimeRep ty1
    rep2 = getRuntimeRep ty2
Ben Gamari's avatar
Ben Gamari committed
735 736 737

repSplitAppTy_maybe (AppTy ty1 ty2)
  = Just (ty1, ty2)
738

ian@well-typed.com's avatar
ian@well-typed.com committed
739
repSplitAppTy_maybe (TyConApp tc tys)
740
  | mightBeUnsaturatedTyCon tc || tys `lengthExceeds` tyConArity tc
741 742
  , Just (tys', ty') <- snocView tys
  = Just (TyConApp tc tys', ty')    -- Never create unsaturated type family apps!
743

744
repSplitAppTy_maybe _other = Nothing
745

746
-- This one doesn't break apart (c => t).
747 748 749 750 751
-- See Note [Decomposing fat arrow c=>t]
-- Defined here to avoid module loops between Unify and TcType.
tcRepSplitAppTy_maybe :: Type -> Maybe (Type,Type)
-- ^ Does the AppTy split as in 'tcSplitAppTy_maybe', but assumes that
-- any coreView stuff is already done. Refuses to look through (c => t)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
752
tcRepSplitAppTy_maybe (FunTy ty1 ty2)
753
  | isPredTy ty1
Ben Gamari's avatar
Ben Gamari committed
754 755
  = Nothing  -- See Note [Decomposing fat arrow c=>t]

756
  | otherwise
Ben Gamari's avatar
Ben Gamari committed
757
  = Just (TyConApp funTyCon [rep1, rep2, ty1], ty2)
758 759 760
  where
    rep1 = getRuntimeRep ty1
    rep2 = getRuntimeRep ty2
Ben Gamari's avatar
Ben Gamari committed
761 762

tcRepSplitAppTy_maybe (AppTy ty1 ty2)    = Just (ty1, ty2)
763 764 765 766 767
tcRepSplitAppTy_maybe (TyConApp tc tys)
  | mightBeUnsaturatedTyCon tc || tys `lengthExceeds` tyConArity tc
  , Just (tys', ty') <- snocView tys
  = Just (TyConApp tc tys', ty')    -- Never create unsaturated type family apps!
tcRepSplitAppTy_maybe _other = Nothing
Ben Gamari's avatar
Ben Gamari committed
768 769 770 771

-- | Like 'tcSplitTyConApp_maybe' but doesn't look through type synonyms.
tcRepSplitTyConApp_maybe :: HasCallStack => Type -> Maybe (TyCon, [Type])
-- Defined here to avoid module loops between Unify and TcType.
772 773 774
tcRepSplitTyConApp_maybe (TyConApp tc tys)
  = Just (tc, tys)

Ben Gamari's avatar
Ben Gamari committed
775 776
tcRepSplitTyConApp_maybe (FunTy arg res)
  = Just (funTyCon, [arg_rep, res_rep, arg, res])
777 778 779
  where
    arg_rep = getRuntimeRep arg
    res_rep = getRuntimeRep res
Ben Gamari's avatar
Ben Gamari committed
780

781 782
tcRepSplitTyConApp_maybe _
  = Nothing
Ben Gamari's avatar
Ben Gamari committed
783

784
-------------
785
splitAppTy :: Type -> (Type, Type)
batterseapower's avatar
batterseapower committed
786 787
-- ^ Attempts to take a type application apart, as in 'splitAppTy_maybe',
-- and panics if this is not possible
788
splitAppTy ty = case splitAppTy_maybe ty of
ian@well-typed.com's avatar
ian@well-typed.com committed
789 790
                Just pr -> pr
                Nothing -> panic "splitAppTy"
791

792
-------------
793
splitAppTys :: Type -> (Type, [Type])
batterseapower's avatar
batterseapower committed
794 795 796
-- ^ Recursively splits a type as far as is possible, leaving a residual
-- type being applied to and the type arguments applied to it. Never fails,
-- even if that means returning an empty list of type applications.
797
splitAppTys ty = split ty ty []
798
  where
799
    split orig_ty ty args | Just ty' <- coreView ty = split orig_ty ty' args
800 801
    split _       (AppTy ty arg)        args = split ty ty (arg:args)
    split _       (TyConApp tc tc_args) args
802
      = let -- keep type families saturated
803 804
            n | mightBeUnsaturatedTyCon tc = 0
              | otherwise                  = tyConArity tc
805
            (tc_args1, tc_args2) = splitAt n tc_args
806 807
        in
        (TyConApp tc tc_args1, tc_args2 ++ args)
Ben Gamari's avatar
Ben Gamari committed
808 809 810
    split _   (FunTy ty1 ty2) args
      = ASSERT( null args )
        (TyConApp funTyCon [], [rep1, rep2, ty1, ty2])
811 812 813
      where
        rep1 = getRuntimeRep ty1
        rep2 = getRuntimeRep ty2
Ben Gamari's avatar
Ben Gamari committed
814 815

    split orig_ty _                     args  = (orig_ty, args)
816

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
817
-- | Like 'splitAppTys', but doesn't look through type synonyms
818
repSplitAppTys :: HasDebugCallStack => Type -> (Type, [Type])
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
819 820 821 822 823 824 825 826 827
repSplitAppTys ty = split ty []
  where
    split (AppTy ty arg) args = split ty (arg:args)
    split (TyConApp tc tc_args) args
      = let n | mightBeUnsaturatedTyCon tc = 0
              | otherwise                  = tyConArity tc
            (tc_args1, tc_args2) = splitAt n tc_args
        in
        (TyConApp tc tc_args1, tc_args2 ++ args)
Ben Gamari's avatar
Ben Gamari committed
828 829 830
    split (FunTy ty1 ty2) args
      = ASSERT( null args )
        (TyConApp funTyCon [], [rep1, rep2, ty1, ty2])
831 832 833
      where
        rep1 = getRuntimeRep ty1
        rep2 = getRuntimeRep ty2
Ben Gamari's avatar
Ben Gamari committed
834

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
835 836
    split ty args = (ty, args)

837
{-
838