search

anoma / juvix

A language for intent-centric and declarative decentralised applications
https://docs.juvix.org
GNU General Public License v3.0
454 stars 53 forks source link

Type synonyms are not always unfolded during type checking #1704

Closed lukaszcz closed 1 year ago

lukaszcz commented 1 year ago

Type checking

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

czero : Num;
czero f x := x;

results in

juvix: too many patterns
CallStack (from HasCallStack):
  error, called at src/Juvix/Prelude/Base.hs:305:9 in juvix-0.2.8-DrlqdRy1M7F1IgVIET4zbg:Juvix.Prelude.Base
  error, called at src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs:308:22 in juvix-0.2.8-DrlqdRy1M7F1IgVIET4zbg:Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Checker
lukaszcz commented 1 year ago

The bigger problem is that type synonyms are not unfolded during type checking, it seems, which makes them largely useless.