reduce sugar in confusing error messages

This addresses the case where you'd see an error of:

Ambiguous elaboration at:
	r <- pure []
Possible correct results:
	[]
	[]
	[]
By changing it to:

Possible correct results:
	Main.Nil
	PrimIO.Nil
	Prelude.Nil
This commit is contained in:
MarcelineVQ 2020-06-20 18:35:02 -07:00 committed by G. Allais
parent 06018ef6c7
commit 6f77c06e3e
2 changed files with 6 additions and 4 deletions

View File

@ -155,7 +155,9 @@ mutual
toPTerm : {auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
(prec : Nat) -> RawImp -> Core PTerm
toPTerm p (IVar fc nm) = toPRef fc nm
toPTerm p (IVar fc nm) = if fullNamespace !(getPPrint)
then pure $ PRef fc nm
else toPRef fc nm
toPTerm p (IPi fc rig Implicit n arg ret)
= do imp <- showImplicits
if imp

View File

@ -64,9 +64,9 @@ Main> (interactive):1:4--1:6:Ambiguous elaboration at:
1 :t []
^^
Possible correct results:
[]
[]
[]
PrimIO.Nil
Prelude.Nil
Data.Vect.Nil
Main> [] : Vect 0 ?elem
Main> [] : List ?a
Main> (interactive):1:34--1:41:When unifying Vect 0 ?elem and List ?a