search

anoma / juvix

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

Crash with cryptic internal error instead of a user-level type error #2771

Closed lukaszcz closed 3 weeks ago

lukaszcz commented 1 month ago

Typechecking

module bug03;

import Stdlib.Data.Nat open;

type Box := mkBox { unbox : Nat };

f (b : Box) : Box :=
  case b of {
    mkBox x := mkBox (x + 1)
  };

main : Nat := f (mkBox 4);

results in

juvix: normalization of case expressions is not supported yet
CallStack (from HasCallStack):
  error, called at src/Juvix/Prelude/Base/Foundation.hs:378:9 in juvix-0.6.1-JZCYqLPdJSb72XcDgw5V5D:Juvix.Prelude.Base.Foundation
  error, called at src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Inference.hs:151:28 in juvix-0.6.1-JZCYqLPdJSb72XcDgw5V5D:Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Inference

Expected behaviour: it should give a type error saying that Box doesn't match Nat.