Fix #1704

[janmasrovira]

• Fixes Type synonyms are not always unfolded during type checking #1704

[lukaszcz]

This doesn't entirely solve the problem. The synonyms are still sometimes not unfolded, e.g., when type-checking a function application.

Checking the module:

module church;

open import Stdlib.Prelude;

Num : Type;
Num := {A : Type} → (A → A) → A → A;

czero : Num;
czero {_} f x := x;

csuc : Num → Num;
csuc n {_} f := f ∘ n f;

end;

results in an error:

Type error near church.juvix:12:21-24.
In the expression:
  n f
the expression n is expected to have a function type but has type:
  Num

[janmasrovira]

The above is now solved, however, you need to provide the implicit argument of n explicitly (due to arity and type checking being in separate stages):

csuc : Num → Num;
csuc n {_} f := f ∘ n {_} f;

[lukaszcz]

Yes, seems to be working now. I can do Church numerals with type synonyms.