Type.hs 118 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,
Ningning Xie's avatar
Ningning Xie committed
18
        Var, TyVar, isTyVar, TyCoVar, TyCoBinder, TyCoVarBinder, TyVarBinder,
19
        KnotTied,
20

batterseapower's avatar
batterseapower committed
21
        -- ** Constructing and deconstructing types
22
        mkTyVarTy, mkTyVarTys, getTyVar, getTyVar_maybe, repGetTyVar_maybe,
Ningning Xie's avatar
Ningning Xie committed
23
        getCastedTyVar_maybe, tyVarKind, varType,
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,
35
        tcRepSplitTyConApp_maybe, tcRepSplitTyConApp, tcSplitTyConApp_maybe,
36 37 38
        splitListTyConApp_maybe,
        repSplitTyConApp_maybe,

Ningning Xie's avatar
Ningning Xie committed
39 40 41 42
        mkForAllTy, mkForAllTys, mkTyCoInvForAllTys, mkSpecForAllTys,
        mkVisForAllTys, mkTyCoInvForAllTy,
        mkInvForAllTy, mkInvForAllTys,
        splitForAllTys, splitForAllVarBndrs,
Simon Peyton Jones's avatar
Simon Peyton Jones committed
43
        splitForAllTy_maybe, splitForAllTy,
Ningning Xie's avatar
Ningning Xie committed
44
        splitForAllTy_ty_maybe, splitForAllTy_co_maybe,
Simon Peyton Jones's avatar
Simon Peyton Jones committed
45
        splitPiTy_maybe, splitPiTy, splitPiTys,
Ningning Xie's avatar
Ningning Xie committed
46 47
        mkTyCoPiTy, mkTyCoPiTys, mkTyConBindersPreferAnon,
        mkPiTys,
Simon Peyton Jones's avatar
Simon Peyton Jones committed
48
        mkLamType, mkLamTypes,
49
        piResultTy, piResultTys,
50
        applyTysX, dropForAlls,
51

52 53
        mkNumLitTy, isNumLitTy,
        mkStrLitTy, isStrLitTy,
54
        isLitTy,
55

56
        getRuntimeRep_maybe, kindRep_maybe, kindRep,
Ben Gamari's avatar
Ben Gamari committed
57

Simon Peyton Jones's avatar
Simon Peyton Jones committed
58
        mkCastTy, mkCoercionTy, splitCastTy_maybe,
59

60
        userTypeError_maybe, pprUserTypeErrorTy,
61

62
        coAxNthLHS,
63 64
        stripCoercionTy, splitCoercionType_maybe,

65 66 67
        splitPiTysInvisible, splitPiTysInvisibleN,
        invisibleTyBndrCount,
        filterOutInvisibleTypes, filterOutInferredTypes,
68 69
        partitionInvisibleTypes, partitionInvisibles,
        tyConArgFlags, appTyArgFlags,
70 71
        synTyConResKind,

lukemaurer's avatar
lukemaurer committed
72 73
        modifyJoinResTy, setJoinResTy,

74 75
        -- Analyzing types
        TyCoMapper(..), mapType, mapCoercion,
ian@well-typed.com's avatar
ian@well-typed.com committed
76 77 78 79 80

        -- (Newtypes)
        newTyConInstRhs,

        -- Pred types
batterseapower's avatar
batterseapower committed
81
        mkFamilyTyConApp,
ian@well-typed.com's avatar
ian@well-typed.com committed
82
        isDictLikeTy,
83 84 85
        mkPrimEqPred, mkReprPrimEqPred, mkPrimEqPredRole,
        equalityTyCon,
        mkHeteroPrimEqPred, mkHeteroReprPrimEqPred,
86
        mkClassPred,
87
        isClassPred, isEqPred, isNomEqPred,
88
        isIPPred, isIPPred_maybe, isIPTyCon, isIPClass,
89
        isCTupleClass,
ian@well-typed.com's avatar
ian@well-typed.com committed
90

batterseapower's avatar
batterseapower committed
91
        -- Deconstructing predicate types
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
92
        PredTree(..), EqRel(..), eqRelRole, classifyPredType,
batterseapower's avatar
batterseapower committed
93
        getClassPredTys, getClassPredTys_maybe,
Joachim Breitner's avatar
Joachim Breitner committed
94
        getEqPredTys, getEqPredTys_maybe, getEqPredRole,
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
95
        predTypeEqRel,
96

97
        -- ** Binders
98
        sameVis,
Ningning Xie's avatar
Ningning Xie committed
99 100
        mkTyCoVarBinder, mkTyCoVarBinders,
        mkTyVarBinders,
101
        mkAnonBinder,
102
        isAnonTyCoBinder,
Ningning Xie's avatar
Ningning Xie committed
103 104 105
        binderVar, binderVars, binderType, binderArgFlag,
        tyCoBinderType, tyCoBinderVar_maybe,
        tyBinderType,
Simon Peyton Jones's avatar
Simon Peyton Jones committed
106
        binderRelevantType_maybe, caseBinder,
107 108
        isVisibleArgFlag, isInvisibleArgFlag, isVisibleBinder,
        isInvisibleBinder, isNamedBinder,
Ningning Xie's avatar
Ningning Xie committed
109
        tyConBindersTyCoBinders,
110

ian@well-typed.com's avatar
ian@well-typed.com committed
111
        -- ** Common type constructors
batterseapower's avatar
batterseapower committed
112
        funTyCon,
113

batterseapower's avatar
batterseapower committed
114
        -- ** Predicates on types
115
        isTyVarTy, isFunTy, isDictTy, isPredTy, isCoercionTy,
116
        isCoercionTy_maybe, isForAllTy,
Ningning Xie's avatar
Ningning Xie committed
117
        isForAllTy_ty, isForAllTy_co,
118
        isPiTy, isTauTy, isFamFreeTy,
119
        isCoVarType, isEvVarType,
batterseapower's avatar
batterseapower committed
120

lukemaurer's avatar
lukemaurer committed
121 122
        isValidJoinPointType,

ian@well-typed.com's avatar
ian@well-typed.com committed
123
        -- (Lifting and boxity)
Richard Eisenberg's avatar
Richard Eisenberg committed
124
        isLiftedType_maybe, isUnliftedType, isUnboxedTupleType, isUnboxedSumType,
125
        isAlgType, isDataFamilyAppType,
ian@well-typed.com's avatar
ian@well-typed.com committed
126
        isPrimitiveType, isStrictType,
127 128
        isRuntimeRepTy, isRuntimeRepVar, isRuntimeRepKindedTy,
        dropRuntimeRepArgs,
129
        getRuntimeRep,
130

ian@well-typed.com's avatar
ian@well-typed.com committed
131
        -- * Main data types representing Kinds
132
        Kind,
batterseapower's avatar
batterseapower committed
133 134

        -- ** Finding the kind of a type
135
        typeKind, tcTypeKind, isTypeLevPoly, resultIsLevPoly,
136
        tcIsLiftedTypeKind, tcIsConstraintKind, tcReturnsConstraintKind,
ian@well-typed.com's avatar
ian@well-typed.com committed
137

138
        -- ** Common Kind
139
        liftedTypeKind,
batterseapower's avatar
batterseapower committed
140

ian@well-typed.com's avatar
ian@well-typed.com committed
141
        -- * Type free variables
142
        tyCoFVsOfType, tyCoFVsBndr, tyCoFVsVarBndr, tyCoFVsVarBndrs,
Simon Peyton Jones's avatar
Simon Peyton Jones committed
143
        tyCoVarsOfType, tyCoVarsOfTypes,
144 145
        tyCoVarsOfTypeDSet,
        coVarsOfType,
Tobias Dammers's avatar
Tobias Dammers committed
146 147 148 149
        coVarsOfTypes,
        closeOverKindsDSet, closeOverKindsFV, closeOverKindsList,
        closeOverKinds,

Richard Eisenberg's avatar
Richard Eisenberg committed
150
        noFreeVarsOfType,
151
        splitVisVarsOfType, splitVisVarsOfTypes,
ian@well-typed.com's avatar
ian@well-typed.com committed
152
        expandTypeSynonyms,
153
        typeSize, occCheckExpand,
154 155

        -- * Well-scoped lists of variables
Tobias Dammers's avatar
Tobias Dammers committed
156 157
        dVarSetElemsWellScoped, scopedSort, tyCoVarsOfTypeWellScoped,
        tyCoVarsOfTypesWellScoped, tyCoVarsOfBindersWellScoped,
158

ian@well-typed.com's avatar
ian@well-typed.com committed
159
        -- * Type comparison
niteria's avatar
niteria committed
160 161
        eqType, eqTypeX, eqTypes, nonDetCmpType, nonDetCmpTypes, nonDetCmpTypeX,
        nonDetCmpTypesX, nonDetCmpTc,
162
        eqVarBndrs,
163

ian@well-typed.com's avatar
ian@well-typed.com committed
164
        -- * Forcing evaluation of types
batterseapower's avatar
batterseapower committed
165
        seqType, seqTypes,
166

batterseapower's avatar
batterseapower committed
167
        -- * Other views onto Types
Ben Gamari's avatar
Ben Gamari committed
168
        coreView, tcView,
batterseapower's avatar
batterseapower committed
169

170
        tyConsOfType,
batterseapower's avatar
batterseapower committed
171

ian@well-typed.com's avatar
ian@well-typed.com committed
172 173
        -- * Main type substitution data types
        TvSubstEnv,     -- Representation widely visible
174
        TCvSubst(..),    -- Representation visible to a few friends
ian@well-typed.com's avatar
ian@well-typed.com committed
175 176

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

niteria's avatar
niteria committed
179
        mkTCvSubst, zipTvSubst, mkTvSubstPrs,
Ningning Xie's avatar
Ningning Xie committed
180
        zipTCvSubst,
181
        notElemTCvSubst,
182
        getTvSubstEnv, setTvSubstEnv,
183
        zapTCvSubst, getTCvInScope, getTCvSubstRangeFVs,
184
        extendTCvInScope, extendTCvInScopeList, extendTCvInScopeSet,
185
        extendTCvSubst, extendCvSubst,
Richard Eisenberg's avatar
Richard Eisenberg committed
186
        extendTvSubst, extendTvSubstBinderAndInScope,
187
        extendTvSubstList, extendTvSubstAndInScope,
Ningning Xie's avatar
Ningning Xie committed
188
        extendTCvSubstList,
189
        extendTvSubstWithClone,
Ningning Xie's avatar
Ningning Xie committed
190
        extendTCvSubstWithClone,
191 192
        isInScope, composeTCvSubstEnv, composeTCvSubst, zipTyEnv, zipCoEnv,
        isEmptyTCvSubst, unionTCvSubst,
193

ian@well-typed.com's avatar
ian@well-typed.com committed
194 195
        -- ** Performing substitution on types and kinds
        substTy, substTys, substTyWith, substTysWith, substTheta,
196 197
        substTyAddInScope,
        substTyUnchecked, substTysUnchecked, substThetaUnchecked,
198
        substTyWithUnchecked,
199
        substCoUnchecked, substCoWithUnchecked,
Simon Peyton Jones's avatar
Simon Peyton Jones committed
200
        substTyVarBndr, substTyVarBndrs, substTyVar, substTyVars,
Ningning Xie's avatar
Ningning Xie committed
201
        substVarBndr, substVarBndrs,
202
        cloneTyVarBndr, cloneTyVarBndrs, lookupTyVar,
203

ian@well-typed.com's avatar
ian@well-typed.com committed
204
        -- * Pretty-printing
205 206
        pprType, pprParendType, pprPrecType,
        pprTypeApp, pprTyThingCategory, pprShortTyThing,
Ningning Xie's avatar
Ningning Xie committed
207
        pprTCvBndr, pprTCvBndrs, pprForAll, pprUserForAll,
208
        pprSigmaType, pprWithExplicitKindsWhen,
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
209
        pprTheta, pprThetaArrowTy, pprClassPred,
dreixel's avatar
dreixel committed
210
        pprKind, pprParendKind, pprSourceTyCon,
211
        PprPrec(..), topPrec, sigPrec, opPrec, funPrec, appPrec, maybeParen,
212
        pprTyVar, pprTyVars,
213
        pprWithTYPE,
Simon Peyton Jones's avatar
Simon Peyton Jones committed
214 215 216 217 218

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

227 228
#include "HsVersions.h"

229 230
import GhcPrelude

lukemaurer's avatar
lukemaurer committed
231 232
import BasicTypes

233
-- We import the representation and primitive functions from TyCoRep.
234 235
-- Many things are reexported, but not the representation!

dreixel's avatar
dreixel committed
236
import Kind
237
import TyCoRep
238

239
-- friends:
240
import Var
241 242
import VarEnv
import VarSet
David Feuer's avatar
David Feuer committed
243
import UniqSet
244

245 246
import Class
import TyCon
247
import TysPrim
Tobias Dammers's avatar
Tobias Dammers committed
248
import {-# SOURCE #-} TysWiredIn ( listTyCon, typeNatKind, unitTy
249 250
                                 , typeSymbolKind, liftedTypeKind
                                 , constraintKind )
251
import PrelNames
252
import CoAxiom
253 254 255 256 257 258 259
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 )
260

261
-- others
262
import Util
Tobias Dammers's avatar
Tobias Dammers committed
263
import FV
264
import Outputable
265
import FastString
266
import Pair
267
import DynFlags  ( gopt_set, GeneralFlag(Opt_PrintExplicitRuntimeReps) )
268
import ListSetOps
269
import Unique ( nonDetCmpUnique )
simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
270

ian@well-typed.com's avatar
ian@well-typed.com committed
271
import Maybes           ( orElse )
Tobias Dammers's avatar
Tobias Dammers committed
272
import Data.Maybe       ( isJust )
273
import Control.Monad    ( guard )
274

batterseapower's avatar
batterseapower committed
275 276
-- $type_classification
-- #type_classification#
ian@well-typed.com's avatar
ian@well-typed.com committed
277
--
batterseapower's avatar
batterseapower committed
278
-- Types are one of:
ian@well-typed.com's avatar
ian@well-typed.com committed
279
--
batterseapower's avatar
batterseapower committed
280
-- [Unboxed]            Iff its representation is other than a pointer
ian@well-typed.com's avatar
ian@well-typed.com committed
281 282
--                      Unboxed types are also unlifted.
--
batterseapower's avatar
batterseapower committed
283
-- [Lifted]             Iff it has bottom as an element.
ian@well-typed.com's avatar
ian@well-typed.com committed
284 285 286 287 288 289
--                      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
290
-- [Algebraic]          Iff it is a type with one or more constructors, whether
ian@well-typed.com's avatar
ian@well-typed.com committed
291 292 293 294 295 296
--                      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
297
-- [Data]               Iff it is a type declared with @data@, or a boxed tuple.
ian@well-typed.com's avatar
ian@well-typed.com committed
298
--
batterseapower's avatar
batterseapower committed
299
-- [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
300
--
batterseapower's avatar
batterseapower committed
301 302
-- 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
303
--
batterseapower's avatar
batterseapower committed
304 305 306
-- 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
307
--
batterseapower's avatar
batterseapower committed
308
-- Some examples of type classifications that may make this a bit clearer are:
ian@well-typed.com's avatar
ian@well-typed.com committed
309
--
batterseapower's avatar
batterseapower committed
310
-- @
311
-- Type          primitive       boxed           lifted          algebraic
batterseapower's avatar
batterseapower committed
312
-- -----------------------------------------------------------------------------
313 314 315 316 317 318
-- 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
319 320 321 322 323
-- @

-- $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
324
-- passes and the rest of the back end is concerned.
batterseapower's avatar
batterseapower committed
325 326 327
--
-- 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
328
-- if they are spotted, to the best of its abilities. If you don't want this
batterseapower's avatar
batterseapower committed
329
-- to happen, use the equivalent functions from the "TcType" module.
330

331 332 333
{-
************************************************************************
*                                                                      *
ian@well-typed.com's avatar
ian@well-typed.com committed
334
                Type representation
335 336
*                                                                      *
************************************************************************
Ben Gamari's avatar
Ben Gamari committed
337 338 339

Note [coreView vs tcView]
~~~~~~~~~~~~~~~~~~~~~~~~~
340 341
So far as the typechecker is concerned, 'Constraint' and 'TYPE
LiftedRep' are distinct kinds.
Ben Gamari's avatar
Ben Gamari committed
342 343 344

But in Core these two are treated as identical.

345 346 347
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.
Ben Gamari's avatar
Ben Gamari committed
348 349 350

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

351
-}
352

Ben Gamari's avatar
Ben Gamari committed
353 354 355
-- | 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.
356
-- See also Note [coreView vs tcView]
Ben Gamari's avatar
Ben Gamari committed
357 358 359 360 361 362 363 364 365 366 367
{-# 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
368

369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390
{-# 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

391 392 393 394 395
-----------------------------------------------
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.
396 397 398
--
-- 'expandTypeSynonyms' only expands out type synonyms mentioned in the type,
-- not in the kinds of any TyCon or TyVar mentioned in the type.
399 400
--
-- Keep this synchronized with 'synonymTyConsOfType'
ian@well-typed.com's avatar
ian@well-typed.com committed
401
expandTypeSynonyms ty
402
  = go (mkEmptyTCvSubst in_scope) ty
403
  where
404 405
    in_scope = mkInScopeSet (tyCoVarsOfType ty)

406
    go subst (TyConApp tc tys)
407 408 409 410 411 412 413 414 415 416
      | 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'
417
      | otherwise
418 419 420 421
      = TyConApp tc expanded_tys
      where
        expanded_tys = (map (go subst) tys)

422 423 424
    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
425
    go subst (FunTy arg res)
426
      = mkFunTy (go subst arg) (go subst res)
Ningning Xie's avatar
Ningning Xie committed
427 428 429
    go subst (ForAllTy (Bndr tv vis) t)
      = let (subst', tv') = substVarBndrUsing go subst tv in
        ForAllTy (Bndr tv' vis) (go subst' t)
430 431 432
    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
433 434 435 436 437 438 439
    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)
440 441 442 443 444 445 446 447
       -- 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
448 449
    go_co subst (FunCo r co1 co2)
      = mkFunCo r (go_co subst co1) (go_co subst co2)
450 451 452 453 454 455 456 457 458 459
    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)
460 461
    go_co subst (NthCo r n co)
      = mkNthCo r n (go_co subst co)
462 463 464 465 466 467 468 469
    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
470 471 472 473
    go_co subst (AxiomRuleCo ax cs)
      = AxiomRuleCo ax (map (go_co subst) cs)
    go_co _ (HoleCo h)
      = pprPanic "expandTypeSynonyms hit a hole" (ppr h)
474 475 476 477 478 479 480

    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
481
      -- substForAllCoBndrUsing, which is general enough to
482 483
      -- handle coercion optimization (which sometimes swaps the
      -- order of a coercion)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
484
    go_cobndr subst = substForAllCoBndrUsing False (go_co subst) subst
485 486 487 488 489 490 491 492 493 494 495 496 497 498

{-
************************************************************************
*                                                                      *
   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.
Ningning Xie's avatar
Ningning Xie committed
499
It stores a TyCoVar and a Coercion, where the kind of the TyCoVar always matches
500 501 502
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
503
The problem is that tcm_tybinder will affect the TyCoVar's kind and
504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529
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
530
                          -- constructors?
531 532
      , tcm_tyvar :: env -> TyVar -> m Type
      , tcm_covar :: env -> CoVar -> m Coercion
Simon Peyton Jones's avatar
Simon Peyton Jones committed
533 534 535
      , tcm_hole  :: env -> CoercionHole -> m Coercion
          -- ^ What to do with coercion holes.
          -- See Note [Coercion holes] in TyCoRep.
536

Ningning Xie's avatar
Ningning Xie committed
537
      , tcm_tycobinder :: env -> TyCoVar -> ArgFlag -> m (env, TyCoVar)
538
          -- ^ The returned env is used in the extended scope
539 540 541 542 543

      , 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
544 545 546
      }

{-# INLINABLE mapType #-}  -- See Note [Specialising mappers]
547
mapType :: Monad m => TyCoMapper env m -> env -> Type -> m Type
548
mapType mapper@(TyCoMapper { tcm_smart = smart, tcm_tyvar = tyvar
Ningning Xie's avatar
Ningning Xie committed
549
                           , tcm_tycobinder = tycobinder, tcm_tycon = tycon })
550 551 552 553 554
        env ty
  = go ty
  where
    go (TyVarTy tv) = tyvar env tv
    go (AppTy t1 t2) = mkappty <$> go t1 <*> go t2
555 556 557 558 559 560
    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
561
    go (FunTy arg res)   = FunTy <$> go arg <*> go res
Ningning Xie's avatar
Ningning Xie committed
562 563
    go (ForAllTy (Bndr tv vis) inner)
      = do { (env', tv') <- tycobinder env tv vis
564
           ; inner' <- mapType mapper env' inner
Ningning Xie's avatar
Ningning Xie committed
565
           ; return $ ForAllTy (Bndr tv' vis) inner' }
Simon Peyton Jones's avatar
Simon Peyton Jones committed
566 567
    go ty@(LitTy {})   = return ty
    go (CastTy ty co)  = mkcastty <$> go ty <*> mapCoercion mapper env co
568 569
    go (CoercionTy co) = CoercionTy <$> mapCoercion mapper env co

Simon Peyton Jones's avatar
Simon Peyton Jones committed
570 571 572
    (mktyconapp, mkappty, mkcastty)
      | smart     = (mkTyConApp, mkAppTy, mkCastTy)
      | otherwise = (TyConApp,   AppTy,   CastTy)
573 574

{-# INLINABLE mapCoercion #-}  -- See Note [Specialising mappers]
575
mapCoercion :: Monad m
576 577
            => TyCoMapper env m -> env -> Coercion -> m Coercion
mapCoercion mapper@(TyCoMapper { tcm_smart = smart, tcm_covar = covar
Ningning Xie's avatar
Ningning Xie committed
578
                               , tcm_hole = cohole, tcm_tycobinder = tycobinder
579
                               , tcm_tycon = tycon })
580 581 582
            env co
  = go co
  where
Ningning Xie's avatar
Ningning Xie committed
583 584 585 586 587
    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)
588
    go (TyConAppCo r tc args)
589 590
      = do { tc' <- tycon tc
           ; mktyconappco r tc' <$> mapM go args }
591 592 593
    go (AppCo c1 c2) = mkappco <$> go c1 <*> go c2
    go (ForAllCo tv kind_co co)
      = do { kind_co' <- go kind_co
Ningning Xie's avatar
Ningning Xie committed
594
           ; (env', tv') <- tycobinder env tv Inferred
595 596 597
           ; 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
598
    go (FunCo r c1 c2) = mkFunCo r <$> go c1 <*> go c2
599 600 601
    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
602
    go (HoleCo hole) = cohole env hole
603 604 605 606 607 608
    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
609
    go (NthCo r i co)      = mknthco r i <$> go co
610 611 612 613 614 615 616 617 618 619 620
    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
621 622
      , mksymco, mktransco, mknthco, mklrco, mkinstco
      , mkkindco, mksubco, mkforallco, mkgreflco)
623 624
      | smart
      = ( mkTyConAppCo, mkAppCo, mkAxiomInstCo, mkUnivCo
Ningning Xie's avatar
Ningning Xie committed
625 626
        , mkSymCo, mkTransCo, mkNthCo, mkLRCo, mkInstCo
        , mkKindCo, mkSubCo, mkForAllCo, mkGReflCo )
627 628
      | otherwise
      = ( TyConAppCo, AppCo, AxiomInstCo, UnivCo
Ningning Xie's avatar
Ningning Xie committed
629 630
        , SymCo, TransCo, NthCo, LRCo, InstCo
        , KindCo, SubCo, ForAllCo, GRefl )
631

632 633 634
{-
************************************************************************
*                                                                      *
635
\subsection{Constructor-specific functions}
636 637
*                                                                      *
************************************************************************
sof's avatar
sof committed
638 639


640
---------------------------------------------------------------------
ian@well-typed.com's avatar
ian@well-typed.com committed
641 642
                                TyVarTy
                                ~~~~~~~
643 644
-}

batterseapower's avatar
batterseapower committed
645 646
-- | 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'
647
getTyVar :: String -> Type -> TyVar
648
getTyVar msg ty = case getTyVar_maybe ty of
ian@well-typed.com's avatar
ian@well-typed.com committed
649 650
                    Just tv -> tv
                    Nothing -> panic ("getTyVar: " ++ msg)
651

652
isTyVarTy :: Type -> Bool
653 654
isTyVarTy ty = isJust (getTyVar_maybe ty)

batterseapower's avatar
batterseapower committed
655
-- | Attempts to obtain the type variable underlying a 'Type'
656
getTyVar_maybe :: Type -> Maybe TyVar
657
getTyVar_maybe ty | Just ty' <- coreView ty = getTyVar_maybe ty'
658 659 660
                  | otherwise               = repGetTyVar_maybe ty

-- | If the type is a tyvar, possibly under a cast, returns it, along
Ningning Xie's avatar
Ningning Xie committed
661
-- with the coercion. Thus, the co is :: kind tv ~N kind ty
662
getCastedTyVar_maybe :: Type -> Maybe (TyVar, CoercionN)
663 664 665 666 667 668 669 670 671 672 673
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
674

675
{-
676
---------------------------------------------------------------------
ian@well-typed.com's avatar
ian@well-typed.com committed
677 678 679
                                AppTy
                                ~~~~~
We need to be pretty careful with AppTy to make sure we obey the
680 681
invariant that a TyConApp is always visibly so.  mkAppTy maintains the
invariant: use it.
682 683 684 685 686

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
687
source Haskell.  In contrast, we *can* unify (a b) with (t1 -> t2).
688 689 690 691 692 693 694 695 696 697 698 699 700 701
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).
702

703
-}
704

batterseapower's avatar
batterseapower committed
705
-- | Applies a type to another, as in e.g. @k a@
706
mkAppTy :: Type -> Type -> Type
707 708
  -- See Note [Respecting definitional equality], invariant (EQ1).
mkAppTy (CastTy fun_ty co) arg_ty
709
  | ([arg_co], res_co) <- decomposePiCos co (coercionKind co) [arg_ty]
710 711
  = (fun_ty `mkAppTy` (arg_ty `mkCastTy` arg_co)) `mkCastTy` res_co

712 713
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
714 715 716 717 718 719 720 721
        -- 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
722

723
mkAppTys :: Type -> [Type] -> Type
ian@well-typed.com's avatar
ian@well-typed.com committed
724
mkAppTys ty1                []   = ty1
725 726 727 728
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
729
  = foldl' AppTy ((mkAppTys fun_ty casted_arg_tys) `mkCastTy` res_co) leftovers
730
  where
731
    (arg_cos, res_co) = decomposePiCos co (coercionKind co) arg_tys
732 733
    (args_to_cast, leftovers) = splitAtList arg_cos arg_tys
    casted_arg_tys = zipWith mkCastTy args_to_cast arg_cos
734
mkAppTys (TyConApp tc tys1) tys2 = mkTyConApp tc (tys1 ++ tys2)
735
mkAppTys ty1                tys2 = foldl' AppTy ty1 tys2
736

737
-------------
738
splitAppTy_maybe :: Type -> Maybe (Type, Type)
batterseapower's avatar
batterseapower committed
739 740 741
-- ^ 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!
742
splitAppTy_maybe ty | Just ty' <- coreView ty
ian@well-typed.com's avatar
ian@well-typed.com committed
743
                    = splitAppTy_maybe ty'
744
splitAppTy_maybe ty = repSplitAppTy_maybe ty
745

746
-------------
747
repSplitAppTy_maybe :: HasDebugCallStack => Type -> Maybe (Type,Type)
ian@well-typed.com's avatar
ian@well-typed.com committed
748
-- ^ Does the AppTy split as in 'splitAppTy_maybe', but assumes that
batterseapower's avatar
batterseapower committed
749
-- any Core view stuff is already done
Ben Gamari's avatar
Ben Gamari committed
750 751
repSplitAppTy_maybe (FunTy ty1 ty2)
  = Just (TyConApp funTyCon [rep1, rep2, ty1], ty2)
752 753 754
  where
    rep1 = getRuntimeRep ty1
    rep2 = getRuntimeRep ty2
Ben Gamari's avatar
Ben Gamari committed
755 756 757

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

ian@well-typed.com's avatar
ian@well-typed.com committed
759
repSplitAppTy_maybe (TyConApp tc tys)
760
  | mightBeUnsaturatedTyCon tc || tys `lengthExceeds` tyConArity tc
761 762
  , Just (tys', ty') <- snocView tys
  = Just (TyConApp tc tys', ty')    -- Never create unsaturated type family apps!
763

764
repSplitAppTy_maybe _other = Nothing
765

766
-- This one doesn't break apart (c => t).
767 768 769 770 771
-- 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
772
tcRepSplitAppTy_maybe (FunTy ty1 ty2)
773
  | isPredTy ty1
Ben Gamari's avatar
Ben Gamari committed
774 775
  = Nothing  -- See Note [Decomposing fat arrow c=>t]

776
  | otherwise
Ben Gamari's avatar
Ben Gamari committed
777
  = Just (TyConApp funTyCon [rep1, rep2, ty1], ty2)
778 779 780
  where
    rep1 = getRuntimeRep ty1
    rep2 = getRuntimeRep ty2
Ben Gamari's avatar
Ben Gamari committed
781 782

tcRepSplitAppTy_maybe (AppTy ty1 ty2)    = Just (ty1, ty2)
783 784 785 786 787
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