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

Agda 2.6.0 compatibility #2

Open
ice1000 opened this issue Nov 14, 2018 · 5 comments
Open

Agda 2.6.0 compatibility #2

ice1000 opened this issue Nov 14, 2018 · 5 comments
Labels
improvements Nice!

Comments

@ice1000
Copy link
Member

ice1000 commented Nov 14, 2018

No description provided.

@ice1000 ice1000 added the improvements Nice! label Nov 14, 2018
@ice1000 ice1000 self-assigned this Nov 14, 2018
@ice1000
Copy link
Member Author

ice1000 commented Nov 14, 2018 

Checking Web.Semantic.Everything (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/Everything.agda).
 Checking Web.Semantic.DL.ABox (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/ABox.agda).
 Checking Web.Semantic.DL.ABox.Interp.Meet (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/ABox/Interp/Meet.agda).
  Checking Web.Semantic.DL.ABox.Interp.Morphism (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/ABox/Interp/Morphism.agda).
   Checking Web.Semantic.DL.TBox.Interp.Morphism (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/TBox/Interp/Morphism.agda).
 Checking Web.Semantic.DL.ABox.Model (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/ABox/Model.agda).
/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/ABox/Model.agda:143,1-14
Don't know how to parse inb (f , I⊨A). Could mean any one of:
  inb (_,_ f I⊨A)
  inb (_,_ f I⊨A)
  inb (_,_ f I⊨A)
  inb (_,_ f I⊨A)
  inb (_,_ f I⊨A)
  inb (_,_ f I⊨A)
Operators used in the grammar:
  , (infixr operator, level 4) [_,_ (/home/ice/.cabal/share/x86_64-linux-ghc-8.4.3/Agda-2.6.0/lib/prim/Agda/Builtin/Sigma.agda:8,15-18)]
  , (infixr operator, level 4) [_,_ (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/ABox.agda:15,3-6)]
  , (infixr operator, level 4) [_,_ (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/ABox/Interp.agda:14,3-6)]
  , (infixr operator, level 4) [_,_ (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/ABox/Interp/Morphism.agda:25,3-6)]
  , (infixr operator, level 4) [_,_ (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/ABox/Interp/Morphism.agda:68,3-6)]
  , (infixr operator, level 5) [_,_ (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/ABox/Model.agda:139,5-8)]
when scope checking the left-hand side inb (f , I⊨A) in the
definition of inb

@ice1000
Copy link
Member Author

ice1000 commented Nov 14, 2018

Is Agda completely losing the ability to use type inference to resolve overloaded operators? @UlfNorell Is this a language change?

@ice1000
Copy link
Member Author

ice1000 commented Nov 14, 2018 •
edited
Loading 

  ((pipe (J , j)) (K , k)) (J≲K , j≲k)
  ((pipe (J , j)) (K , k)) (J≲K , j≲k)
  ((pipe (J , j)) (K , k)) (J≲K , j≲k)
  ((pipe (J , j)) (K , k)) (J≲K , j≲k)
  ((pipe (J , j)) (K , k)) (J≲K , j≲k)
  ((pipe (J , j)) (K , k)) (J≲K , j≲k)
  ((pipe (J , j)) (K , k)) (J≲K , j≲k)
  ((pipe (J , j)) (K , k)) (J≲K , j≲k)
  ((pipe (J , j)) (K , k)) (J≲K , j≲k)
  ((pipe (J , j)) (K , k)) (J≲K , j≲k)
  ((pipe (J , j)) (K , k)) (J≲K , j≲k)
  ((pipe (J , j)) (K , k)) (J≲K , j≲k)
  ((pipe (J , j)) (K , k)) (J≲K , j≲k)
  ((pipe (J , j)) (K , k)) (J≲K , j≲k)
  ((pipe (J , j)) (K , k)) (J≲K , j≲k)
  ((pipe (J , j)) (K , k)) (J≲K , j≲k)
  ((pipe (J , j)) (K , k)) (J≲K , j≲k)
  ((pipe (J , j)) (K , k)) (J≲K , j≲k)
  ((pipe (J , j)) (K , k)) (J≲K , j≲k)
Operators used in the grammar:
  , (infixr operator, level 4) [_,_ (/home/ice/.cabal/share/x86_64-linux-ghc-8.4.3/Agda-2.6.0/lib/prim/Agda/Builtin/Sigma.agda:8,15-18)]
  , (infixr operator, level 4) [_,_ (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/ABox.agda:15,3-6)]
  , (infixr operator, level 4) [_,_ (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/ABox/Interp.agda:14,3-6)]
  , (infixr operator, level 4) [_,_ (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/ABox/Interp/Morphism.agda:25,3-6)]
  , (infixr operator, level 4) [_,_ (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/ABox/Interp/Morphism.agda:68,3-6)]
  , (infixr operator, level 4) [_,_ (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/Category/Morphism.agda:25,3-6)]
  , (infixr operator, level 4) [_,_ (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/Category/Morphism.agda:30,3-6)]
  , (infixr operator, level 4) [_,_ (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/Category/Morphism.agda:77,3-6)]
  , (infixr operator, level 4) [_,_ (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/Category/Object.agda:13,3-6)]
  , (infixr operator, level 4) [_,_ (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/Integrity.agda:44,5-8)]
  , (infixr operator, level 4) [_,_ (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/Integrity.agda:65,3-6)]
  , (infixr operator, level 4) [_,_ (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/Integrity.agda:84,5-8)]
  , (infixr operator, level 4) [_,_ (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/KB.agda:10,3-6)]
  , (infixr operator, level 4) [_,_ (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/TBox.agda:14,3-6)]
  , (infixr operator, level 5) [_,_ (/home/ice/SDK/agda-web-semantic/src/Web/Semantic/DL/ABox/Model.agda:139,5-8)]
when scope checking the left-hand side
pipe (J , j) (K , k) (J≲K , j≲k) in the definition of pipe

@ice1000 ice1000 removed their assignment Nov 14, 2018
@ice1000
Copy link
Member Author

ice1000 commented Nov 14, 2018

My Agda compiler is built from 2d980891f570cf4a50b8e8843eb9c5269b4d888e commit in the compiler repo

@gallais
Copy link
Member

gallais commented Nov 14, 2018

If you make sure that all _,_ have the same fixity level then it should fix the issue, I believe.

bblfish added a commit to bblfish/agda-web-semantic that referenced this issue Jan 2, 2021
@bblfish
fix for agda#2
9c94736
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
improvements Nice!
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@gallais @ice1000