Some issues and workarounds when writing interfaces

(See Interfaces for introduction on how to split a module between an interface and its implementation.)

This page lists some issues and workarounds when using interfaces.

Declaring a type in the interface and defining it in the implementation

This currently does not work:

A.fsti:

module A

type t :Type

and

A.fst:

module A

type t = nat

In general the interfaces do not play well with a type definition split like this. Instead use the val and let syntax:

A.fsti:

module A

val t :Type

and

A.fst:

module A

let t = nat

But this also doesn't work, see the next bullet.

Generalization of universes problem

The code above gives a universe error, because of a known issue with generalization of val being separate from let (see this github issue). The solution is to be more explicit with universes:

A.fsti:

module A

val t :Type0

and

A.fst:

module A

let t = nat

Higher universe types can also be specified with the explicit universe syntax.

But this doesn't work if the type you want to define is an inductive, see the next bullet.

Separating the declaration and definition in the case of inductives

This currently doesn't work:

A.fsti:

module A

val t :Type0

and

A.fst:

module A

let t =
  | C: nat -> t

The reason is that let cannot be used to define inductives currently. Instead the workaround is to define a private type, and then using it in the let:

A.fsti:

module A

val t :Type0

and

A.fst:

module A

private type t' =
  | C: nat -> t'

let t = t'

let definitions at the end of an interface

Interfaces can also have let definitions, but currently there seems to be a bug that does not allow let definitions to be the last top-level things in the interface file, e.g. this gives an error currently:

A.fsti:

module A

val t :Type0

let foo = unit

and

A.fst:

module A

let t = nat

whereas this works fine:

A.fsti:

module A

let foo = unit

val t :Type0

and

A.fst:

module A

let t = nat

Issue with the logic qualifier

The following example gives an error about Inconsistent logic qualifier:

A.fsti:

module A

val foo :Type0

and

A.fst:

module A

let foo = True \/ True

This is a known issue. The workaround, as also discussed in the issue, is to write a dummy let in the .fst:

A.fst:

module A

let foo =
  let _ = () in
  True \/ True