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

Misleading error messages in mutual definitions. #3499

Open
semenov-vladyslav opened this issue Jan 13, 2019 · 3 comments
Open

Misleading error messages in mutual definitions. #3499

semenov-vladyslav opened this issue Jan 13, 2019 · 3 comments
Labels
copatterns Definitions by copattern matching: projections on the LHS mutual parser Problems with the parser's implementation (rather than with decisions about syntax) scope Issues relating to scope checking
Milestone
icebox

Comments

@semenov-vladyslav
Copy link
Contributor 

module test where

postulate
  A : Set

f : A → A
g : A → A

f g = {!!}
g x = {!!}

The message is the following:

test.agda:9,1-4
More than one matching type signature for left hand side f g it
could belong to any of:
g (at test.agda:7,1-2)
f (at test.agda:6,1-2)

If the definition of f is moved before g is declared or the g argument to f is renamed than everything of course is fine.

If the definition of f is moved after the definition of g then the error message is different:

———— Error —————————————————————————————————————————————————
test.agda:10,1-4
Could not parse the left-hand side f g
Operators used in the grammar:
  None
when scope checking the left-hand side f g in the definition of g

———— Warning(s) ————————————————————————————————————————————
test.agda:6,1-2
The following names are declared but not accompanied by a
definition: f

Is this behaviour expected?
@ice1000
Copy link
Member

ice1000 commented Jan 20, 2019

For the flipped version, maybe Agda tries to parse definitions like

f a : Bla
g f = bla

as a "copattern matching", which is kind of problematic.

Adding {-# OPTIONS --no-copatterns #-} does not resolves this.

@ice1000 ice1000 added the parser Problems with the parser's implementation (rather than with decisions about syntax) label Jan 20, 2019
@ice1000
Copy link
Member

ice1000 commented Jan 20, 2019

Renaming the variables can be a workaround.

@ice1000 ice1000 added the copatterns Definitions by copattern matching: projections on the LHS label Jan 20, 2019
@andreasabel andreasabel added mutual scope Issues relating to scope checking labels Jan 21, 2019
@andreasabel
Copy link
Member

The problem is that the assignment of clauses to functions happens even before scope checking in https://github.com/agda/agda/blob/master/src/full/Agda/Syntax/Concrete/Definitions.hs and the heuristics to assign a function clause to a name is necessarily very crude:

agda/src/full/Agda/Syntax/Concrete/Definitions.hs

Lines 1279 to 1305 in 38cbf84

couldBeFunClauseOf :: Maybe Fixity' -> Name -> Declaration -> Bool
couldBeFunClauseOf mFixity x (Pragma (CatchallPragma{})) = True
couldBeFunClauseOf mFixity x (FunClause (LHS p _ _) _ _ _) = hasEllipsis p ||
let
pns = patternNames p
xStrings = nameStringParts x
patStrings = concatMap nameStringParts pns
in
-- trace ("x = " ++ prettyShow x) $
-- trace ("pns = " ++ show pns) $
-- trace ("xStrings = " ++ show xStrings) $
-- trace ("patStrings = " ++ show patStrings) $
-- trace ("mFixity = " ++ show mFixity) $
case (headMaybe pns, mFixity) of
-- first identifier in the patterns is the fun.symbol?
(Just y, _) | x == y -> True -- trace ("couldBe since y = " ++ prettyShow y) $ True
-- are the parts of x contained in p
_ | xStrings `isSublistOf` patStrings -> True -- trace ("couldBe since isSublistOf") $ True
-- looking for a mixfix fun.symb
(_, Just fix) -> -- also matches in case of a postfix
let notStrings = stringParts (theNotation fix)
in -- trace ("notStrings = " ++ show notStrings) $
-- trace ("patStrings = " ++ show patStrings) $
(not $ null notStrings) && (notStrings `isSublistOf` patStrings)
-- not a notation, not first id: give up
_ -> False -- trace ("couldBe not (case default)") $ False
couldBeFunClauseOf _ _ _ = False -- trace ("couldBe not (fun default)") $ False

@UlfNorell made some initial efforts to get rid of this pre-pass, then (doing it in the scope checker) the heuristics could be way better.

@jespercockx jespercockx added this to the icebox milestone Feb 11, 2019
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
copatterns Definitions by copattern matching: projections on the LHS mutual parser Problems with the parser's implementation (rather than with decisions about syntax) scope Issues relating to scope checking
Projects
None yet
Milestone
icebox
Development

No branches or pull requests
4 participants
@andreasabel @jespercockx @semenov-vladyslav @ice1000