# How exactly do type constraints work?
**URL:** https://discuss.ocaml.org/t/how-exactly-do-type-constraints-work/7630
**Category:** Learning
**Created:** [April 9, 2021, 3:38am UTC](https://discuss.ocaml.org/t/how-exactly-do-type-constraints-work/7630 "2021-04-09T03:38:46Z")
**Posts on this page:** 5
**Page:** 1
### Author:  [@joelb](https://discuss.ocaml.org/u/joelb)
#### Post date: [April 9, 2021, 3:38am UTC](https://discuss.ocaml.org/t/how-exactly-do-type-constraints-work/7630/1 "2021-04-09T03:38:46Z")
Hi all, I have two modules, `A` and `B`, which I’d like to type with signatures as shown below. These modules are recursive (`A.t` refers to `B.t` and vice-versa), but I’d like their signatures to be independent, both because I want to give them separate names and to avoid [unexpected (?) typing error related to aliasing of types defined in recursive modules · Issue #7622 · ocaml/ocaml · GitHub](https://github.com/ocaml/ocaml/issues/7622).
```auto
module type A_s = sig
type b_t
type t = Empty_a | A_of_b of b_t
end
module type B_s = sig
type a_t
type t = Empty_b | B_of_a of a_t
end
module type S = sig
type a_t
type b_t
module Term : A_s with type t = a_t and type b_t = b_t
module Scope : B_s with type t = b_t and type a_t = a_t
end
```
My hope was that by including `b_t` in `A_s` and `a_t` in `B_s` I could write the signatures without reference to each other. Unfortunately this doesn’t compile with a message that (I don’t really think makes sense, but) seems to be the same as in the Github issue linked above.
```auto
❯ ocaml test.ml
File "./test.ml", line 14, characters 25-37:
14 | module Term : A_s with type t = a_t and type b_t = b_t
^^^^^^^^^^^^
Error: This variant or record definition does not match that of type a_t
Their kinds differ.
```
I also tried a variation on this:
```auto
module type S = sig
type a_t = Empty_a | A_of_b of b_t
and b_t = Empty_b | B_of_a of a_t
module Term : A_s with type t = a_t and type b_t = b_t
module Scope : B_s with type t = b_t and type a_t = a_t
end
```
No luck.
```auto
❯ ocaml test.ml
File "./test.ml", line 14, characters 25-37:
14 | module Term : A_s with type t = a_t and type b_t = b_t
^^^^^^^^^^^^
Error: This variant or record definition does not match that of type a_t
Constructors do not match:
A_of_b of b_t
is not compatible with:
A_of_b of b_t/2
The types are not equal.
```
So, my question is twofold. (1) Is there a way to do what I’m trying? (hopefully it’s clear) And (2) what’s a good source of information on how type constraints work? The OCaml manual is great but doesn’t seem to go into as much depth as I need here.
---
### Author:  [@octachron](https://discuss.ocaml.org/u/octachron)
#### Post date: [April 9, 2021, 7:56am UTC](https://discuss.ocaml.org/t/how-exactly-do-type-constraints-work/7630/2 "2021-04-09T07:56:52Z")
Your second variant works if your order correctly the substitutions:
```ocaml
module type S = sig
type a_t = Empty_a | A_of_b of b_t
and b_t = Empty_b | B_of_a of a_t
module Term : A_s with type b_t = b_t and type t = a_t
module Scope : B_s with type a_t = a_t and type t = b_t
end
```
---
### Author:  [@shonfeder](https://discuss.ocaml.org/u/shonfeder)
#### Post date: [April 9, 2021, 10:22am UTC](https://discuss.ocaml.org/t/how-exactly-do-type-constraints-work/7630/3 "2021-04-09T10:22:04Z")
What determines the correctness of the order here?
---
### Author:  [@octachron](https://discuss.ocaml.org/u/octachron)
#### Post date: [April 9, 2021, 10:30am UTC](https://discuss.ocaml.org/t/how-exactly-do-type-constraints-work/7630/4 "2021-04-09T10:30:13Z")
In brief, the substitutions are done in order.
The substitution `with type b_t = b_t` adds the equality between the type `b_t` defined in `A_s` and the external type `b_t`. This substitution is always valid because `b_t` is abstract in `A_s`.
The second substitution ` with type t = a_t` adds an equality the two types. However, since the definition of `a_t` in `A_s` is not abstract, the two definitions must match. In other words, the `A_s` version of
```ocaml
type a_t = Empty_a | A_of_b of b_t
```
should be compatible with the outer `S` version. This is only the case if the inner `b_t` in `A_s` and the outer `b_t` in `S` are equal.
---
### Author:  [@joelb](https://discuss.ocaml.org/u/joelb)
#### Post date: [April 9, 2021, 2:55pm UTC](https://discuss.ocaml.org/t/how-exactly-do-type-constraints-work/7630/5 "2021-04-09T14:55:46Z")
Thanks @octachron! This was exactly what I needed.
I ended up using octachron’s solution, with the small tweak of destructive substitution, to prevent exposing `a_t` and `b_t`.
```auto
module type S = sig
type a_t = Empty_a | A_of_b of b_t
and b_t = Empty_b | B_of_a of a_t
module Term : A_s with type b_t := b_t and type t = a_t
module Scope : B_s with type a_t := a_t and type t = b_t
end
```
Also, I’ve only started to read it, but Leroy’s [_Manifest types, modules, and separate compilation_](https://caml.inria.fr/pub/papers/xleroy-manifest_types-popl94.pdf) looks like a good reference.