Don't crash on parse errors in deriving clauses

[anka-213]

It turns out that if you don't specify a file-name, then the Haskell parser haskell-src-exts uses the filename <unknown>.hs,
which we afterwards try to parse as an absolute filepath to extract the location of the error, which causes a crash.

Since the location from the Haskell parser wouldn't be accurate anyways, we change it to just report the entire pragma as the location of the error.

This PR also makes the code for converting Haskell locations into Agda locations return Nothing for the filename, instead of crashing if there is no valid filename in the error. This might not be desired since we should be able to provide a more helpful filename and location and this could make it easier to miss the issues with bad error reporting. That change currently has no impact, since this PR also prevents it from triggering.

Fixes #351

[anka-213]

It would also be possible to adjust the haskell parser to have a more accurate location, using similar code to the one used for foreign pragmas:

agda2hs/src/Agda2Hs/Pragma.hs

Lines 38 to 45 in 22f37f5

	let Just file = fmap (filePath . rangeFilePath) $ toLazy $ rangeFile r
	pmode = Hs.defaultParseMode { Hs.parseFilename = file,
	Hs.ignoreLinePragmas = False,
	Hs.extensions = exts }
	line = case posLine <$> rStart r of
	Just l -> "{-# LINE " ++ show l ++ show file ++ " #-}\n"
	Nothing -> ""
	case Hs.parseWithComments pmode (line ++ code) of

The issue with that is that we don't know exactly how far into the line the deriving keyword is, so it's difficult to adjust the column number accurately in the haskell parser.

It might however be worthwhile to provide the list of extensions to the haskell parser for deriving clauses, like the FOREIGN parser does, so it can accurately handle things like "deriving via", but that's a separate unrelated issue that would require more refactoring.

[jespercockx]

Thanks for the PR! I generally agree that having a more precise error location would be nice but here the issue seems rather minor so I would propose just merging this PR as is.

[anka-213]

I agree. I believe that getting the more precise location reliably is currently blocked by getting more range information from the Agda parser.

More specifically: We only get the range of the full pragma, not the range of the string contents we get from it, so the best we could do is to guess that there is only one whitespace between each keyword and calculate how long the {-# COMPILE AGDA2HS FunctionName prefix should be and then subtract that or make the dummy data type declaration have the exact same length, so that the haskell error message gets an accurate location most of the time.

[jespercockx]

Ok, then let's go ahead and merge this.

[anka-213]

@jespercockx btw, on a related note: the code currently doesn't report an error on invalid keywords after {-# COMPILE AGDA2HS FunctionName, but instead just ignores them. Is this intended behavior?

In the function

agda2hs/src/Agda2Hs/Pragma.hs

Lines 85 to 102 in 22f37f5

	processPragma :: QName -> C ParsedPragma
	processPragma qn = liftTCM (getUniqueCompilerPragma pragmaName qn) >>= \case
	Nothing -> return NoPragma
	Just (CompilerPragma _ s)
	| "class" `isPrefixOf` s -> return $ ClassPragma (words $ drop 5 s)
	| s == "inline" -> return InlinePragma
	| s == "existing-class" -> return ExistingClassPragma
	| s == "unboxed" -> return $ UnboxPragma Lazy
	| s == "unboxed-strict" -> return $ UnboxPragma Strict
	| s == "transparent" -> return TransparentPragma
	| s == "tuple" -> return $ TuplePragma Hs.Boxed
	| s == "unboxed-tuple" -> return $ TuplePragma Hs.Unboxed
	| s == newtypePragma -> return $ NewTypePragma []
	| s == derivePragma -> return $ DerivePragma Nothing
	| derivePragma `isPrefixOf` s -> return $ DerivePragma (parseStrategy (drop (length derivePragma + 1) s))
	| "deriving" `isPrefixOf` s -> processDeriving s DefaultPragma
	| (newtypePragma ++ " deriving") `isPrefixOf` s -> processDeriving (drop (length newtypePragma + 1) s) NewTypePragma
	_ -> return $ DefaultPragma []

The final line ignores errors:

agda2hs/src/Agda2Hs/Pragma.hs

Line 102 in 22f37f5

_ -> return $ DefaultPragma []

This means that this is accepted:

record Foo : Set where
{-# COMPILE AGDA2HS Foo "&"€%(€&( #-}

However, getting precise error location for this would have the same issue, so we would have to either give an imprecise error or make a guess (that will be true 99% of the time). But I guess the lack of precision doesn't matter too much there either.

[jespercockx]

I'm not sure if it's intentional or not, I think it's been like that since the original implementation by @UlfNorell