Note [Concrete types]
Definition: a type is /concrete/ iff it is:
- a concrete type constructor (as defined below), or
- a concrete type variable (see Note [ConcreteTv] below), or
- an application of a concrete type to another concrete type
GHC.Core.Type.isConcreteType checks whether a type meets this definition.
Definition: a /concrete type constructor/ is defined by
- a promoted data constructor
- a class, data type or newtype
- a primitive type like Array# or Int#
- an abstract type as defined in a Backpack signature file
(see Note [Synonyms implement abstract data] in GHC.Tc.Module)
In particular, type and data families are not concrete.
GHC.Core.TyCon.isConcreteTyCon checks whether a TyCon meets this definition.
Examples of concrete types:
Lifted, BoxedRep Lifted, TYPE (BoxedRep Lifted) are all concrete
Examples of non-concrete types
F Int, TYPE (F Int), TYPE r, a[sk]
NB: (F Int) is not concrete because F is a type function
The recursive definition of concreteness entails the following property:
Concrete Congruence Property (CCP)
All sub-trees of a concrete type tree are concrete.
The following property also holds due to the invariant that the kind of a
concrete metavariable is itself concrete (see Note [ConcreteTv]):
Concrete Kinds Property (CKP)
The kind of a concrete type is concrete. References 2
- Synonyms implement abstract data GHC.Tc.Module
- ConcreteTv GHC.Tc.Utils.Concrete
Referenced by 15
- GHC.Core.Type call site ×2
- GHC.Tc.Utils.Concrete call site ×2
- GHC.Tc.Utils.TcType call site ×2
- GHC.Tc.Utils.Unify call site ×2
- Preserve RuntimeRep info in cast w/w GHC.Core.Opt.Simplify.Iteration
- GHC.Core.TyCon call site
- Eta-expanding rep-poly unlifted newtypes GHC.Tc.Gen.App
- ConcreteTv GHC.Tc.Utils.Concrete
- Fixed RuntimeRep GHC.Tc.Utils.Concrete
- Concrete overview GHC.Tc.Utils.Concrete
- GHC.Tc.Utils.TcMType call site