This module contains functions to generate instances for supported typeclasses for user-defined Haskell data types.

Suppose we have a type > data T α₁ … αₙ = C₁ τ₍₁,₁₎ … τ₍₁,ₘ₁₎ | … | Cₖ τ₍ₖ,₁₎ … τ₍ₖ,ₘₖ₎. We wish to generate an instance of class C providing the function f : T α₁ … αₙ -> τ, where τ is a type. For example, for the Normalform class, f would be > nf' : T α₁ … αₙ -> Free Shape Pos (T α₁ … αₙ).

The generated function has the following basic structure:

f'T < class-specific binders > (x : T α₁ … αₙ) : B
     := match x with
        | C₁ fx₍₁,₁₎ … fx₍₁,ₘ₁₎ => < buildValue x [fx₍₁,₁₎, …, fx₍₁,ₘ₁₎ >
        | …
        | Cₖ fx₍ₖ,₁₎ … fx₍ₖ,ₘₖ₎ => < buildValue x [fx₍ₖ,₁₎, …, fxk₍ₖ,ₘₖ₎] >
        end.

buildValue x [fx₍ᵢ,₁₎, …, fx₍ᵢ,ₘᵢ₎] represents class-specific code that actually constructs a value of type τ when given x and the constructor's parameters as arguments.

For example, for a Normalform instance of a type data List a = Nil | Cons a (List a), the function would look as follows.

nf'List_ {Shape : Type} {Pos : Shape -> Type}
         {a b : Type} `{Normalform Shape Pos a b}
         (x : List Shape Pos a)
  : Free Shape Pos (List Identity.Shape Identity.Pos b)
     := match x with
        | nil => pure nil
        | cons fx_0 fx_1 => nf fx_0 >>= fun nx_0 =>
                            fx_1 >>= fun x_1 =>
                            nf'List x_1 >>= fun nx_1 =>
                            pure (cons (pure nx_0) (pure nx_1))
        end.

Typically, buildValue will use the class function f on all components, then reconstruct the value using the results of those function calls. In the example above, we use nf on fx_0 of type a. nf fx_0 means the same as fx_0 >>= fun x_0 => nf' x_0.

Since we translate types in topological order and C instances exist for all previously translated types (and types from the Prelude), we can use f on most arguments. For all type variables, we introduce class constraints into the type signature of the function. However, this is not possible for (indirectly) recursive arguments.

A directly recursive argument has the type T τ₁ … τₙ, where τᵢ is a type expressions (not necessarily type variables). We assume that τᵢ' does not contain T for any i, as this would constitute a non-positive occurrence of T and make T invalid in Coq. For these arguments, instead of the function f we call fT recursively.

An indirectly recursive argument is an argument of a type that is not T, but contains T. These arguments are problematic because we can neither use f on them (as that would generally require a C instance of T) nor can we use fT.

The problem is solved by introducing a local function fT' for every type T' that contains T that inlines the definition of a T' instance of C, and call this function for arguments of type T'. These local functions are as polymorphic as possible to reduce the number of local functions we need.

For example, if we want to generate an instance for the Haskell type

data Forest a = AForest [Forest a]
              | IntForest [Forest Int]
              | BoolForest [Forest Bool]

only one local function is needed. In the case of Normalform, the local function would look as follows.

nf'ListForest_ {a b : Type} `{Normalform Shape Pos a b}
  : List Shape Pos (Forest Shape Pos a)
  -> Free Shape Pos (List Identity.Shape Identity.Pos
                    (Forest Identity.Shape Identity.Pos b))

To generate these local functions, for every type expression τ₍ᵢ,ⱼ₎ in the constructors of T, we collect all types that contain the original type T. More specifically, a type expression T' τ₁ … τₙ is collected if τᵢ = T τ₁' … τₙ' for some type expressions τ₁, …, τₙ, or if τᵢ is collected for some i. During this process, any type expression that does not contain T is replaced by a placeholder variable _.

We keep track of which types correspond to which function with a map.

The generated functions fT₁, …, fTₙ for n mutually recursive types T₁, … Tₙ are a set of n Fixpoint definitions linked with with. Indirectly recursive types and local functions based on them are computed for each type. In this case, a type T' is considered indirectly recursive if it contains any of the types T₁, …, Tₙ. Arguments of type Tᵢ can be treated like directly recursive arguments.