I am just a hobbier who doesn't major in Computational Science and Engineering.
Recently, I made a tiny functional programming language: https://github.com/mecheng98/nabi
But nabi is untyped, so I want to add a type-checker to it.
It is a concrete goal that I implement a type-checker which is based on haskell98 but supports the only extension "associated type synonyms".
I read the paper Associated Type Synonyms right then tried to make the constraint-entailment function (||-).
But I failed to do it, because it is too hard for me to have (||-) apply the inference rule "EQ_subst" and not fall into infinite loop.
Would you please to give me a hint to make (||-) and teach me how to achieve my goal?
+) I hope to represent types in THIH style.
Thank you very much to read my question. Happy New Year.
I read the paper Associated Type Synonyms right then tried to make the constraint-entailment function (||-).
But I failed to do it, because it is too hard for me to have (||-) apply the inference rule "EQ_subst" and not fall into infinite loop.
It sounds like trying to implement the typing rules directly (Figure 2), but those alone don't give an effective type checking procedure. The paper also presents a type inference algorithm (Section 5; Figures 4, 5), that's what should be implemented. To follow that section, you might want to first have a good grasp of Hindley-Milner type inference and unification.