Note [Concrete types]

GHC/Tc/Utils/Concrete.hs:178 compiler

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

Referenced by 15