Skip to content

Commit

Permalink
Fix bug in isTrait (#2368)
Browse files Browse the repository at this point in the history
* Closes #2367
  • Loading branch information
lukaszcz authored Sep 14, 2023
1 parent f84dcb4 commit 487fc58
Show file tree
Hide file tree
Showing 3 changed files with 6 additions and 2 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -15,8 +15,8 @@ type SubsI = HashMap VarName InstanceParam
subsIToE :: SubsI -> SubsE
subsIToE = fmap paramToExpression

isTrait :: InfoTable -> InductiveName -> Bool
isTrait tab name = fromJust (HashMap.lookup name (tab ^. infoInductives)) ^. inductiveInfoDef . inductiveTrait
isTrait :: InfoTable -> Name -> Bool
isTrait tab name = maybe False (^. inductiveInfoDef . inductiveTrait) (HashMap.lookup name (tab ^. infoInductives))

resolveTraitInstance ::
(Members '[Error TypeCheckerError, NameIdGen, Inference, Reader LocalVars, Reader InfoTable] r) =>
Expand Down
1 change: 1 addition & 0 deletions tests/Compilation/positive/out/test061.out
Original file line number Diff line number Diff line change
Expand Up @@ -10,4 +10,5 @@ just (true) :: nothing :: just (false) :: nil
just (1 :: nil) :: nothing :: just (2 :: 3 :: nil) :: nil
abba
abba!
abba3
a :: b :: c :: d :: nil
3 changes: 3 additions & 0 deletions tests/Compilation/positive/test061.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -47,6 +47,8 @@ f'3 {A} {{M : Show A}} : A → String := Show.show {{M}};

f'4 {A} {{_ : Show A}} : A → String := Show.show;

f5 {A} {{Show A}} (n : String) (a : A) : String := n ++str Show.show a;

main : IO :=
printStringLn (Show.show true) >>
printStringLn (f false) >>
Expand All @@ -60,4 +62,5 @@ main : IO :=
printStringLn (f'4 [just [1]; nothing; just [2; 3]]) >>
printStringLn (f'3 "abba") >>
printStringLn (f'3 {{M := mkShow (λ{x := x ++str "!"})}} "abba") >>
printStringLn (f5 "abba" 3) >>
printStringLn (Show.show ["a"; "b"; "c"; "d"]);

0 comments on commit 487fc58

Please sign in to comment.