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

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

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

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

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

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

48 49
        mkNumLitTy, isNumLitTy,
        mkStrLitTy, isStrLitTy,
50

Ben Gamari's avatar
Ben Gamari committed
51 52
        getRuntimeRep_maybe, getRuntimeRepFromKind_maybe,

Simon Peyton Jones's avatar
Simon Peyton Jones committed
53
        mkCastTy, mkCoercionTy, splitCastTy_maybe,
54

55
        userTypeError_maybe, pprUserTypeErrorTy,
56

57
        coAxNthLHS,
58 59 60 61 62 63
        stripCoercionTy, splitCoercionType_maybe,

        splitPiTysInvisible, filterOutInvisibleTypes,
        filterOutInvisibleTyVars, partitionInvisibles,
        synTyConResKind,

lukemaurer's avatar
lukemaurer committed
64 65
        modifyJoinResTy, setJoinResTy,

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

        -- (Newtypes)
        newTyConInstRhs,

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

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

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

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

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

lukemaurer's avatar
lukemaurer committed
109 110
        isValidJoinPointType,

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

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

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

125
        -- ** Common Kind
126
        liftedTypeKind,
batterseapower's avatar
batterseapower committed
127

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

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

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

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

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

154
        tyConsOfType,
batterseapower's avatar
batterseapower committed
155

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

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

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

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

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

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

206 207
#include "HsVersions.h"

lukemaurer's avatar
lukemaurer committed
208 209
import BasicTypes

210
-- We import the representation and primitive functions from TyCoRep.
211 212
-- Many things are reexported, but not the representation!

dreixel's avatar
dreixel committed
213
import Kind
214
import TyCoRep
215

216
-- friends:
217
import Var
218 219
import VarEnv
import VarSet
David Feuer's avatar
David Feuer committed
220
import UniqSet
221

222 223
import Class
import TyCon
224
import TysPrim
225 226 227
import {-# SOURCE #-} TysWiredIn ( listTyCon, typeNatKind
                                 , typeSymbolKind, liftedTypeKind )
import PrelNames
228
import CoAxiom
229
import {-# SOURCE #-} Coercion
230

231
-- others
232
import Util
233
import Outputable
234
import FastString
235 236 237
import Pair
import ListSetOps
import Digraph
238
import Unique ( nonDetCmpUnique )
239 240 241
import SrcLoc  ( SrcSpan )
import OccName ( OccName )
import Name    ( mkInternalName )
simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
242

ian@well-typed.com's avatar
ian@well-typed.com committed
243
import Maybes           ( orElse )
244
import Data.Maybe       ( isJust, mapMaybe )
245
import Control.Monad    ( guard )
246
import Control.Arrow    ( first, second )
247

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

-- $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
297
-- passes and the rest of the back end is concerned.
batterseapower's avatar
batterseapower committed
298 299 300 301 302
--
-- 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.
303

304 305 306
{-
************************************************************************
*                                                                      *
ian@well-typed.com's avatar
ian@well-typed.com committed
307
                Type representation
308 309
*                                                                      *
************************************************************************
Ben Gamari's avatar
Ben Gamari committed
310 311 312 313 314 315 316 317 318 319 320 321

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.

322
-}
323 324 325

{-# INLINE coreView #-}
coreView :: Type -> Maybe Type
326 327
-- ^ This function Strips off the /top layer only/ of a type synonym
-- application (if any) its underlying representation type.
328
-- Returns Nothing if there is nothing to look through.
Ben Gamari's avatar
Ben Gamari committed
329
-- This function considers 'Constraint' to be a synonym of @TYPE LiftedRep@.
330
--
331 332
-- By being non-recursive and inlined, this case analysis gets efficiently
-- joined onto the case analysis that the caller is already doing
333
coreView (TyConApp tc tys) | Just (tenv, rhs, tys') <- expandSynTyCon_maybe tc tys
niteria's avatar
niteria committed
334
  = Just (mkAppTys (substTy (mkTvSubstPrs tenv) rhs) tys')
335 336
               -- The free vars of 'rhs' should all be bound by 'tenv', so it's
               -- ok to use 'substTy' here.
337
               -- See also Note [The substitution invariant] in TyCoRep.
batterseapower's avatar
batterseapower committed
338
               -- Its important to use mkAppTys, rather than (foldl AppTy),
ian@well-typed.com's avatar
ian@well-typed.com committed
339
               -- because the function part might well return a
batterseapower's avatar
batterseapower committed
340
               -- partially-applied type constructor; indeed, usually will!
Ben Gamari's avatar
Ben Gamari committed
341 342 343 344
coreView (TyConApp tc [])
  | isStarKindSynonymTyCon tc
  = Just liftedTypeKind

345
coreView _ = Nothing
346

Ben Gamari's avatar
Ben Gamari committed
347 348 349 350 351 352 353 354 355 356 357 358 359 360 361
-- | 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.
-- See also Note [coreView vs tcView] in Type.
{-# 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
362

363 364 365 366 367
-----------------------------------------------
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.
368 369 370
--
-- 'expandTypeSynonyms' only expands out type synonyms mentioned in the type,
-- not in the kinds of any TyCon or TyVar mentioned in the type.
371 372
--
-- Keep this synchronized with 'synonymTyConsOfType'
ian@well-typed.com's avatar
ian@well-typed.com committed
373
expandTypeSynonyms ty
374
  = go (mkEmptyTCvSubst in_scope) ty
375
  where
376 377
    in_scope = mkInScopeSet (tyCoVarsOfType ty)

378
    go subst (TyConApp tc tys)
379 380 381 382 383 384 385 386 387 388
      | 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'
389
      | otherwise
390 391 392 393
      = TyConApp tc expanded_tys
      where
        expanded_tys = (map (go subst) tys)

394 395 396
    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
397
    go subst (FunTy arg res)
398
      = mkFunTy (go subst arg) (go subst res)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
399
    go subst (ForAllTy (TvBndr tv vis) t)
400
      = let (subst', tv') = substTyVarBndrCallback go subst tv in
Simon Peyton Jones's avatar
Simon Peyton Jones committed
401
        ForAllTy (TvBndr tv' vis) (go subst' t)
402 403 404 405 406 407 408 409 410 411 412 413 414
    go subst (CastTy ty co)  = mkCastTy (go subst ty) (go_co subst co)
    go subst (CoercionTy co) = mkCoercionTy (go_co subst co)

    go_co subst (Refl r ty)
      = mkReflCo r (go subst ty)
       -- 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
415 416
    go_co subst (FunCo r co1 co2)
      = mkFunCo r (go_co subst co1) (go_co subst co2)
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 458 459 460 461 462 463 464 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
    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)
    go_co subst (NthCo n co)
      = mkNthCo n (go_co subst co)
    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 (CoherenceCo co1 co2)
      = mkCoherenceCo (go_co subst co1) (go_co subst co2)
    go_co subst (KindCo co)
      = mkKindCo (go_co subst co)
    go_co subst (SubCo co)
      = mkSubCo (go_co subst co)
    go_co subst (AxiomRuleCo ax cs) = AxiomRuleCo ax (map (go_co subst) cs)

    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
    go_prov _     (HoleProv h)        = pprPanic "expandTypeSynonyms hit a hole" (ppr h)

      -- the "False" and "const" are to accommodate the type of
      -- substForAllCoBndrCallback, which is general enough to
      -- handle coercion optimization (which sometimes swaps the
      -- order of a coercion)
    go_cobndr subst = substForAllCoBndrCallback False (go_co subst) subst

{-
************************************************************************
*                                                                      *
   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
                         -- constructors?
      , tcm_tyvar :: env -> TyVar -> m Type
      , tcm_covar :: env -> CoVar -> m Coercion
      , tcm_hole  :: env -> CoercionHole -> Role
                  -> Type -> Type -> m Coercion
          -- ^ What to do with coercion holes. See Note [Coercion holes] in
          -- TyCoRep.

505
      , tcm_tybinder :: env -> TyVar -> ArgFlag -> m (env, TyVar)
506 507 508 509
          -- ^ The returned env is used in the extended scope
      }

{-# INLINABLE mapType #-}  -- See Note [Specialising mappers]
510
mapType :: Monad m => TyCoMapper env m -> env -> Type -> m Type
511 512 513 514 515 516 517
mapType mapper@(TyCoMapper { tcm_smart = smart, tcm_tyvar = tyvar
                           , tcm_tybinder = tybinder })
        env ty
  = go ty
  where
    go (TyVarTy tv) = tyvar env tv
    go (AppTy t1 t2) = mkappty <$> go t1 <*> go t2
518 519
    go t@(TyConApp _ []) = return t  -- avoid allocation in this exceedingly
                                     -- common case (mostly, for *)
520
    go (TyConApp tc tys) = mktyconapp tc <$> mapM go tys
Simon Peyton Jones's avatar
Simon Peyton Jones committed
521 522
    go (FunTy arg res)   = FunTy <$> go arg <*> go res
    go (ForAllTy (TvBndr tv vis) inner)
523 524
      = do { (env', tv') <- tybinder env tv vis
           ; inner' <- mapType mapper env' inner
Simon Peyton Jones's avatar
Simon Peyton Jones committed
525 526 527
           ; return $ ForAllTy (TvBndr tv' vis) inner' }
    go ty@(LitTy {})   = return ty
    go (CastTy ty co)  = mkcastty <$> go ty <*> mapCoercion mapper env co
528 529
    go (CoercionTy co) = CoercionTy <$> mapCoercion mapper env co

Simon Peyton Jones's avatar
Simon Peyton Jones committed
530 531 532
    (mktyconapp, mkappty, mkcastty)
      | smart     = (mkTyConApp, mkAppTy, mkCastTy)
      | otherwise = (TyConApp,   AppTy,   CastTy)
533 534

{-# INLINABLE mapCoercion #-}  -- See Note [Specialising mappers]
535
mapCoercion :: Monad m
536 537 538 539 540 541 542 543 544 545 546 547
            => TyCoMapper env m -> env -> Coercion -> m Coercion
mapCoercion mapper@(TyCoMapper { tcm_smart = smart, tcm_covar = covar
                               , tcm_hole = cohole, tcm_tybinder = tybinder })
            env co
  = go co
  where
    go (Refl r ty) = Refl r <$> mapType mapper env ty
    go (TyConAppCo r tc args)
      = mktyconappco r tc <$> mapM go args
    go (AppCo c1 c2) = mkappco <$> go c1 <*> go c2
    go (ForAllCo tv kind_co co)
      = do { kind_co' <- go kind_co
548
           ; (env', tv') <- tybinder env tv Inferred
549 550 551
           ; 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
552
    go (FunCo r c1 c2) = mkFunCo r <$> go c1 <*> go c2
553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587
    go (CoVarCo cv) = covar env cv
    go (AxiomInstCo ax i args)
      = mkaxiominstco ax i <$> mapM go args
    go (UnivCo (HoleProv hole) r t1 t2)
      = cohole env hole r t1 t2
    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
    go (NthCo i co)        = mknthco i <$> go co
    go (LRCo lr co)        = mklrco lr <$> go co
    go (InstCo co arg)     = mkinstco <$> go co <*> go arg
    go (CoherenceCo c1 c2) = mkcoherenceco <$> go c1 <*> go c2
    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
    go_prov (HoleProv _)        = panic "mapCoercion"

    ( mktyconappco, mkappco, mkaxiominstco, mkunivco
      , mksymco, mktransco, mknthco, mklrco, mkinstco, mkcoherenceco
      , mkkindco, mksubco, mkforallco)
      | smart
      = ( mkTyConAppCo, mkAppCo, mkAxiomInstCo, mkUnivCo
        , mkSymCo, mkTransCo, mkNthCo, mkLRCo, mkInstCo, mkCoherenceCo
        , mkKindCo, mkSubCo, mkForAllCo )
      | otherwise
      = ( TyConAppCo, AppCo, AxiomInstCo, UnivCo
        , SymCo, TransCo, NthCo, LRCo, InstCo, CoherenceCo
        , KindCo, SubCo, ForAllCo )
588

589 590 591
{-
************************************************************************
*                                                                      *
592
\subsection{Constructor-specific functions}
593 594
*                                                                      *
************************************************************************
sof's avatar
sof committed
595 596


597
---------------------------------------------------------------------
ian@well-typed.com's avatar
ian@well-typed.com committed
598 599
                                TyVarTy
                                ~~~~~~~
600 601
-}

batterseapower's avatar
batterseapower committed
602 603
-- | 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'
604
getTyVar :: String -> Type -> TyVar
605
getTyVar msg ty = case getTyVar_maybe ty of
ian@well-typed.com's avatar
ian@well-typed.com committed
606 607
                    Just tv -> tv
                    Nothing -> panic ("getTyVar: " ++ msg)
608

609
isTyVarTy :: Type -> Bool
610 611
isTyVarTy ty = isJust (getTyVar_maybe ty)

batterseapower's avatar
batterseapower committed
612
-- | Attempts to obtain the type variable underlying a 'Type'
613
getTyVar_maybe :: Type -> Maybe TyVar
614
getTyVar_maybe ty | Just ty' <- coreView ty = getTyVar_maybe ty'
615 616 617
                  | otherwise               = repGetTyVar_maybe ty

-- | If the type is a tyvar, possibly under a cast, returns it, along
618 619
-- with the coercion. Thus, the co is :: kind tv ~N kind type
getCastedTyVar_maybe :: Type -> Maybe (TyVar, CoercionN)
620 621 622 623 624 625 626 627 628 629 630
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
631

632
{-
633
---------------------------------------------------------------------
ian@well-typed.com's avatar
ian@well-typed.com committed
634 635 636
                                AppTy
                                ~~~~~
We need to be pretty careful with AppTy to make sure we obey the
637 638
invariant that a TyConApp is always visibly so.  mkAppTy maintains the
invariant: use it.
639 640 641 642 643

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
644
source Haskell.  In contrast, we *can* unify (a b) with (t1 -> t2).
645 646 647 648 649 650 651 652 653 654 655 656 657 658
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).
659

660
-}
661

batterseapower's avatar
batterseapower committed
662
-- | Applies a type to another, as in e.g. @k a@
663
mkAppTy :: Type -> Type -> Type
664 665
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
666 667 668 669 670 671 672 673
        -- 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
674

675
mkAppTys :: Type -> [Type] -> Type
ian@well-typed.com's avatar
ian@well-typed.com committed
676
mkAppTys ty1                []   = ty1
677 678 679
mkAppTys (TyConApp tc tys1) tys2 = mkTyConApp tc (tys1 ++ tys2)
mkAppTys ty1                tys2 = foldl AppTy ty1 tys2

680
-------------
681
splitAppTy_maybe :: Type -> Maybe (Type, Type)
batterseapower's avatar
batterseapower committed
682 683 684
-- ^ 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!
685
splitAppTy_maybe ty | Just ty' <- coreView ty
ian@well-typed.com's avatar
ian@well-typed.com committed
686
                    = splitAppTy_maybe ty'
687
splitAppTy_maybe ty = repSplitAppTy_maybe ty
688

689 690
-------------
repSplitAppTy_maybe :: Type -> Maybe (Type,Type)
ian@well-typed.com's avatar
ian@well-typed.com committed
691
-- ^ Does the AppTy split as in 'splitAppTy_maybe', but assumes that
batterseapower's avatar
batterseapower committed
692
-- any Core view stuff is already done
Ben Gamari's avatar
Ben Gamari committed
693 694 695 696 697 698 699 700 701
repSplitAppTy_maybe (FunTy ty1 ty2)
  | Just rep1 <- getRuntimeRep_maybe ty1
  , Just rep2 <- getRuntimeRep_maybe ty2
  = Just (TyConApp funTyCon [rep1, rep2, ty1], ty2)

  | otherwise
  = pprPanic "repSplitAppTy_maybe" (ppr ty1 $$ ppr ty2)
repSplitAppTy_maybe (AppTy ty1 ty2)
  = Just (ty1, ty2)
ian@well-typed.com's avatar
ian@well-typed.com committed
702
repSplitAppTy_maybe (TyConApp tc tys)
703
  | mightBeUnsaturatedTyCon tc || tys `lengthExceeds` tyConArity tc
704 705
  , Just (tys', ty') <- snocView tys
  = Just (TyConApp tc tys', ty')    -- Never create unsaturated type family apps!
706
repSplitAppTy_maybe _other = Nothing
707 708 709 710 711 712 713

-- this one doesn't braek apart (c => t).
-- 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
714
tcRepSplitAppTy_maybe (FunTy ty1 ty2)
Ben Gamari's avatar
Ben Gamari committed
715 716 717 718 719 720 721 722 723 724
  | isConstraintKind (typeKind ty1)
  = Nothing  -- See Note [Decomposing fat arrow c=>t]

  | Just rep1 <- getRuntimeRep_maybe ty1
  , Just rep2 <- getRuntimeRep_maybe ty2
  = Just (TyConApp funTyCon [rep1, rep2, ty1], ty2)

  | otherwise
  = pprPanic "repSplitAppTy_maybe" (ppr ty1 $$ ppr ty2)
tcRepSplitAppTy_maybe (AppTy ty1 ty2)    = Just (ty1, ty2)
725 726 727 728 729
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
730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756

-- | Split a type constructor application into its type constructor and
-- applied types. Note that this may fail in the case of a 'FunTy' with an
-- argument of unknown kind 'FunTy' (e.g. @FunTy (a :: k) Int@. since the kind
-- of @a@ isn't of the form @TYPE rep@). Consequently, you may need to zonk your
-- type before using this function.
--
-- If you only need the 'TyCon', consider using 'tcTyConAppTyCon_maybe'.
tcSplitTyConApp_maybe :: HasCallStack => Type -> Maybe (TyCon, [Type])
-- Defined here to avoid module loops between Unify and TcType.
tcSplitTyConApp_maybe ty | Just ty' <- tcView ty = tcSplitTyConApp_maybe ty'
tcSplitTyConApp_maybe ty                         = tcRepSplitTyConApp_maybe ty

-- | 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.
tcRepSplitTyConApp_maybe (TyConApp tc tys)          = Just (tc, tys)
tcRepSplitTyConApp_maybe (FunTy arg res)
  | Just arg_rep <- getRuntimeRep_maybe arg
  , Just res_rep <- getRuntimeRep_maybe res
  = Just (funTyCon, [arg_rep, res_rep, arg, res])

  | otherwise
  = pprPanic "tcRepSplitTyConApp_maybe" (ppr arg $$ ppr res)
tcRepSplitTyConApp_maybe _                          = Nothing


757
-------------
758
splitAppTy :: Type -> (Type, Type)
batterseapower's avatar
batterseapower committed
759 760
-- ^ Attempts to take a type application apart, as in 'splitAppTy_maybe',
-- and panics if this is not possible
761
splitAppTy ty = case splitAppTy_maybe ty of
ian@well-typed.com's avatar
ian@well-typed.com committed
762 763
                Just pr -> pr
                Nothing -> panic "splitAppTy"
764

765
-------------
766
splitAppTys :: Type -> (Type, [Type])
batterseapower's avatar
batterseapower committed
767 768 769
-- ^ 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.
770
splitAppTys ty = split ty ty []
771
  where
772
    split orig_ty ty args | Just ty' <- coreView ty = split orig_ty ty' args
773 774
    split _       (AppTy ty arg)        args = split ty ty (arg:args)
    split _       (TyConApp tc tc_args) args
775
      = let -- keep type families saturated
776 777
            n | mightBeUnsaturatedTyCon tc = 0
              | otherwise                  = tyConArity tc
778
            (tc_args1, tc_args2) = splitAt n tc_args
779 780
        in
        (TyConApp tc tc_args1, tc_args2 ++ args)
Ben Gamari's avatar
Ben Gamari committed
781 782 783 784 785 786 787 788 789
    split _   (FunTy ty1 ty2) args
      | Just rep1 <- getRuntimeRep_maybe ty1
      , Just rep2 <- getRuntimeRep_maybe ty2
      = ASSERT( null args )
        (TyConApp funTyCon [], [rep1, rep2, ty1, ty2])

      | otherwise
      = pprPanic "splitAppTys" (ppr ty1 $$ ppr ty2 $$ ppr args)
    split orig_ty _                     args  = (orig_ty, args)
790

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
791 792 793 794 795 796 797 798 799 800 801
-- | Like 'splitAppTys', but doesn't look through type synonyms
repSplitAppTys :: Type -> (Type, [Type])
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
802 803 804 805 806 807 808 809
    split (FunTy ty1 ty2) args
      | Just rep1 <- getRuntimeRep_maybe ty1
      , Just rep2 <- getRuntimeRep_maybe ty2
      = ASSERT( null args )
        (TyConApp funTyCon [], [rep1, rep2, ty1, ty2])

      | otherwise
      = pprPanic "repSplitAppTys" (ppr ty1 $$ ppr ty2 $$ ppr args)
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
810 811
    split ty args = (ty, args)

812
{-
813
                      LitTy
814
                      ~~~~~
815
-}
816

817 818
mkNumLitTy :: Integer -> Type
mkNumLitTy n = LitTy (NumTyLit n)
819

820
-- | Is this a numeric literal. We also look through type synonyms.
821
isNumLitTy :: Type -> Maybe Integer
822
isNumLitTy ty | Just ty1 <- coreView ty = isNumLitTy ty1
823 824
isNumLitTy (LitTy (NumTyLit n)) = Just n
isNumLitTy _                    = Nothing
825

826 827 828
mkStrLitTy :: FastString -> Type
mkStrLitTy s = LitTy (StrTyLit s)

829
-- | Is this a symbol literal. We also look through type synonyms.
830
isStrLitTy :: Type -> Maybe FastString
831
isStrLitTy ty | Just ty1 <- coreView ty = isStrLitTy ty1
832 833
isStrLitTy (LitTy (StrTyLit s)) = Just s
isStrLitTy _                    = Nothing
834

835 836 837

-- | Is this type a custom user error?
-- If so, give us the kind and the error message.
838 839
userTypeError_maybe :: Type -> Maybe Type
userTypeError_maybe t
840 841 842 843
  = do { (tc, _kind : msg : _) <- splitTyConApp_maybe t
          -- There may be more than 2 arguments, if the type error is
          -- used as a type constructor (e.g. at kind `Type -> Type`).

844 845
       ; guard (tyConName tc == errorMessageTypeErrorFamName)
       ; return msg }
846 847 848 849 850 851 852 853 854 855 856 857 858 859 860 861 862 863 864 865 866 867 868 869 870 871 872 873 874 875 876

-- | Render a type corresponding to a user type error into a SDoc.
pprUserTypeErrorTy :: Type -> SDoc
pprUserTypeErrorTy ty =
  case splitTyConApp_maybe ty of

    -- Text "Something"
    Just (tc,[txt])
      | tyConName tc == typeErrorTextDataConName
      , Just str <- isStrLitTy txt -> ftext str

    -- ShowType t
    Just (tc,[_k,t])
      | tyConName tc == typeErrorShowTypeDataConName -> ppr t

    -- t1 :<>: t2
    Just (tc,[t1,t2])
      | tyConName tc == typeErrorAppendDataConName ->
        pprUserTypeErrorTy t1 <> pprUserTypeErrorTy t2

    -- t1 :$$: t2
    Just (tc,[t1,t2])
      | tyConName tc == typeErrorVAppendDataConName ->
        pprUserTypeErrorTy t1 $$ pprUserTypeErrorTy t2

    -- An uneavaluated type function
    _ -> ppr ty




877
{-
878
---------------------------------------------------------------------
ian@well-typed.com's avatar
ian@well-typed.com committed
879 880
                                FunTy
                                ~~~~~
Ben Gamari's avatar
Ben Gamari committed
881 882 883 884 885 886 887 888 889