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

Polymorphic axiom results in an exception #1338

Closed
lukaszcz opened this issue Jul 7, 2022 · 2 comments · Fixed by #1386
Closed

Polymorphic axiom results in an exception #1338

lukaszcz opened this issue Jul 7, 2022 · 2 comments · Fixed by #1386
Assignees
@lukaszcz
Labels
bug error-messaging language typechecking
Milestone
0.2.2

Comments

@lukaszcz
Copy link
Collaborator

lukaszcz commented Jul 7, 2022

Compiling:

module bug1;

inductive Unit{
  unit : Unit;
};

axiom fun : {A : Type} -> A -> Unit;

end;

results in:

minijuvix: the given type is not concrete
CallStack (from HasCallStack):
  error, called at src/MiniJuvix/Prelude/Base.hs:264:9 in minijuvix-0.2.0-AhwHxl28r3k6kLaQ64J4z7:MiniJuvix.Prelude.Base
  error, called at src/MiniJuvix/Syntax/MicroJuvix/Language/Extra.hs:83:14 in minijuvix-0.2.0-AhwHxl28r3k6kLaQ64J4z7:MiniJuvix.Syntax.MicroJuvix.Language.Extra
@janmasrovira
Copy link
Collaborator

#1341 should fix this

@cwgoes cwgoes transferred this issue from another repository Jul 13, 2022
@jonaprieto jonaprieto added this to the 0.2.2 milestone Jul 14, 2022
@lukaszcz
Copy link
Collaborator Author

Confirmed, PR #1386 fixes this

@jonaprieto jonaprieto mentioned this issue Jul 18, 2022
Merged
7 tasks
@jonaprieto jonaprieto linked a pull request Jul 18, 2022 that will close this issue
Direct translation from MicroJuvix to MiniC #1386
Merged
7 tasks
lukaszcz added a commit that referenced this issue Jul 18, 2022
@lukaszcz
Direct translation from MicroJuvix to MiniC.
4e5a4bc 
* Closes issues #1341, #1338, #1339.
* Depends on PR [#8](anoma/juvix-stdlib#8) in juvix-stdlib.
* Translation/MonoJuvixToMiniC removed.
* MonoJuvix itself not removed because the MiniHaskell backend depends on it.
* Since MiniHaskell is deprecated, I see no point in wasting time on writing a translation from MicroJuvix to MiniHaskell.
lukaszcz added a commit that referenced this issue Jul 18, 2022
@lukaszcz
Add tests for issues #1338 and #1339
bd98f0c
lukaszcz added a commit that referenced this issue Jul 18, 2022
@lukaszcz
Direct translation from MicroJuvix to MiniC.
cb0f334 
* Closes issues #1341, #1338, #1339.
* Depends on PR [#8](anoma/juvix-stdlib#8) in juvix-stdlib.
* Translation/MonoJuvixToMiniC removed.
* MonoJuvix itself not removed because the MiniHaskell backend depends on it.
* Since MiniHaskell is deprecated, I see no point in wasting time on writing a translation from MicroJuvix to MiniHaskell.
lukaszcz added a commit that referenced this issue Jul 18, 2022
@lukaszcz
Add tests for issues #1338 and #1339
a3362b8
lukaszcz added a commit that referenced this issue Jul 19, 2022
@lukaszcz
Direct translation from MicroJuvix to MiniC.
6d26a91 
* Closes issues #1341, #1338, #1339.
* Depends on PR [#8](anoma/juvix-stdlib#8) in juvix-stdlib.
* Translation/MonoJuvixToMiniC removed.
* MonoJuvix itself not removed because the MiniHaskell backend depends on it.
* Since MiniHaskell is deprecated, I see no point in wasting time on writing a translation from MicroJuvix to MiniHaskell.
lukaszcz added a commit that referenced this issue Jul 19, 2022
@lukaszcz
Add tests for issues #1338 and #1339
40cf024
lukaszcz added a commit that referenced this issue Jul 19, 2022
@lukaszcz
Direct translation from MicroJuvix to MiniC.
8070cdd 
* Closes issues #1341, #1338, #1339.
* Depends on PR [#8](anoma/juvix-stdlib#8) in juvix-stdlib.
* Translation/MonoJuvixToMiniC removed.
* MonoJuvix itself not removed because the MiniHaskell backend depends on it.
* Since MiniHaskell is deprecated, I see no point in wasting time on writing a translation from MicroJuvix to MiniHaskell.
lukaszcz added a commit that referenced this issue Jul 19, 2022
@lukaszcz
Add tests for issues #1338 and #1339
1d03048
lukaszcz added a commit that referenced this issue Jul 19, 2022
@lukaszcz
Direct translation from MicroJuvix to MiniC.
44a908d 
* Closes issues #1341, #1338, #1339.
* Depends on PR [#8](anoma/juvix-stdlib#8) in juvix-stdlib.
* Translation/MonoJuvixToMiniC removed.
* MonoJuvix itself not removed because the MiniHaskell backend depends on it.
* Since MiniHaskell is deprecated, I see no point in wasting time on writing a translation from MicroJuvix to MiniHaskell.
lukaszcz added a commit that referenced this issue Jul 19, 2022
@lukaszcz
Add tests for issues #1338 and #1339
cb3656c
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@lukaszcz lukaszcz

Labels
bug error-messaging language typechecking
Projects
None yet
Milestone
0.2.2
Development

Successfully merging a pull request may close this issue.

Direct translation from MicroJuvix to MiniC anoma/juvix
3 participants
@lukaszcz @jonaprieto @janmasrovira