Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

The translation from Internal to Core doesn't work with type synonyms #1714

Closed
lukaszcz opened this issue Jan 10, 2023 · 0 comments · Fixed by #1728
Closed

The translation from Internal to Core doesn't work with type synonyms #1714

lukaszcz opened this issue Jan 10, 2023 · 0 comments · Fixed by #1728
Labels
bug internal-to-core
Milestone
0.3 - Valencia

Comments

@lukaszcz
Copy link
Collaborator

Trying to evaluate the following via core

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;

toNat : Num → Nat;
toNat n := n {_} ((+) 1) 0;

main : IO;
main :=
  printNatLn (toNat (csuc (czero)));

end;

gives the error

juvix: impossible
CallStack (from HasCallStack):
  error, called at src/Juvix/Prelude/Base.hs:315:14 in juvix-0.2.8-DyFVJXJWeol4IAnBe15XnM:Juvix.Prelude.Base
  impossible, called at src/Juvix/Compiler/Core/Translation/FromInternal.hs:526:34 in juvix-0.2.8-DyFVJXJWeol4IAnBe15XnM:Juvix.Compiler.Core.Translation.FromInternal
@lukaszcz lukaszcz added this to the 0.3 milestone Jan 10, 2023
@paulcadman paulcadman mentioned this issue Jan 16, 2023
Merged
paulcadman added a commit that referenced this issue Jan 16, 2023
@paulcadman
Do not filter implicit args in internal to core translation (#1728)
ff748b9 
The internal to core translation was removing implicit arguments from
function definitions and applications. This is incorrect as the implicit
bindings are required when translating the following (in `csuc`, the
binding of the implicit argument is required in an application on the
rhs):

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

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

Apart from removing this filter from function and application
translation, this required the following changes:

ConstructorInfo:
The _constructorArgsNum field must include the number of type parameters
of its inductive type.

PatternConstructorApp:
The pattern arguments must include wildcards for the implicit type
parameters passed to the constructor.

BuiltinIf:
The BuiltinIf expression is passed an implicit type argument that must
be removed when translating to Core if.

LitString:
A literal string is a function with an implcit type argument. So this
must be a translated to a lambda where the type argument is ignored.

Fixes #1714
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
bug internal-to-core
Projects
None yet
Milestone
0.3 - Valencia
Development

Successfully merging a pull request may close this issue.

Do not filter implicit args in internal to core translation anoma/juvix
2 participants
@lukaszcz @jonaprieto