Module Generic_core_equal

module Generic_core_equal: sig .. end

Type equality predicate.

type ('_, '_) equal =

`\|`	`Refl : ('a, 'a) equal`

x : ('a,'b) equal is a witness that 'a and 'b are intensionally equal.

Pattern matching x with Refl will force the type checker to unify 'a and 'b.

type ('a, 'b) t = ('a, 'b) equal

type equal_fun = {

f : 'a 'b. 'a Ty.t -> 'b Ty.t -> ('a, 'b) equal option;

}

val ext : 'a Ty.pat -> equal_fun -> unit

extends equal with a new case.

val equal : 'a Ty.t ->
       'b Ty.t -> ('a, 'b) equal option

val coerce : 'a Ty.t -> 'b Ty.t -> 'a -> 'b option

Coerces a value between two intensionally equal types. In other words, ('a, 'b) equal must be inhabited for a value of type 'a to be coerced into the type 'b.