Stream: General

Topic: Type unification problem

view this post on Zulip Gergely Buday (Mar 19 2024 at 16:49):

I get this type unification problem:

Operator:  (∘) CONSTRUCTION.rtf ::
  ('a::type M N M ⇒ ??'a::type CONSTRUCTION.M CONSTRUCTION.N CONSTRUCTION.M)
  ⇒ 'a::type M N M ⇒ ??'a::type CONSTRUCTION.N CONSTRUCTION.M
Operand:   expr :: 'a::type M N M ⇒ 'b::type M N M

I wonder why ??'a in the Operator type cannot be unified with 'b in the Operand type. Isn't ??'a a schematic type variable that could be unified with 'b?

view this post on Zulip Mathias Fleury (Mar 19 2024 at 16:51):

Given the error message, I suspect that CONSTRUCTION.M and M are distinct

view this post on Zulip Gergely Buday (Mar 19 2024 at 16:52):

By definition, they are equal, and so are

CONSTRUCTION.N = N

view this post on Zulip Mathias Fleury (Mar 19 2024 at 16:54):

Tthe error message is mixing both and type_synonym is introducing a synonym that is expanded in the error message. So how are you doing the "by definition they are equal"?

Last updated: Dec 21 2024 at 12:33 UTC