search

UlfNorell / agda-test

Agda test
0 stars 0 forks source link

Error message points to importing module rather than imported module #623

Open UlfNorell opened 10 years ago

UlfNorell commented 10 years ago

From nils.anders.danielsson on May 06, 2012 19:39:08

A.agda:

module A where

open import B

B.agda:

module B where

S : Set S = Set

$ agda A.agda Checking A (A.agda). Checking B (B.agda). Finished B. A.agda:3,1-14 Termination checking failed for the following functions: S Problematic calls: S (at B.agda:4,5-6) when scope checking the declaration open import B

I think the error should be raised before we print "Finished B.", and that the error's range should point to B, not A.

The error is raised in getInterface:

getInterface :: ModuleName -> TCM (Interface, ClockTime) getInterface x = do (i, wt) <- getInterface' (toTopLevelModuleName x) False case wt of Left w -> typeError $ warningsToError w Right t -> return (i, t)

Original issue: http://code.google.com/p/agda/issues/detail?id=623

UlfNorell commented 10 years ago

From andreas....@gmail.com on May 07, 2012 12:18:06

Did you mean to write

S = S

? Otherwise you should rather get an universe error...

Labels: Priority-Medium Modules

UlfNorell commented 10 years ago

From nils.anders.danielsson on May 08, 2012 01:51:33

Did you mean to write

S = S

?

Yes.

UlfNorell commented 10 years ago

From ulf.nor...@gmail.com on May 09, 2012 03:30:23

What exactly should the range be? The first problematic call in B?

UlfNorell commented 10 years ago

From nils.anders.danielsson on May 09, 2012 07:00:11

That's one choice. We could also combine the ranges of all calls, but that wouldn't work so well unless we stopped applying continuousPerLine to error ranges.