Fix type rendering for existentials, other tweaks

This commit is contained in:
Rúnar 2024-01-26 12:53:29 -05:00
parent 887d9acca5
commit 3b7e2586a2
6 changed files with 87 additions and 43 deletions

View File

@ -646,18 +646,27 @@ renderTypeError e env src = case e of
C.WrongType -> (_2 %~ (s :)) . r
C.WrongName -> (_3 %~ (s :)) . r
undefinedSymbolHelp =
Pr.wrap $
mconcat
[ mconcat ["Its type should conform to ", style Type1 (renderType' env expectedType)],
Pr.hang
"Some common causes of this error include:"
( Pr.bulleted
[ Pr.wrap "Your current namespace is too deep to contain the definition in its subtree",
Pr.wrap "The definition is part of a library which hasn't been added to this project",
Pr.wrap "You have a typo in the name"
mconcat
[ ( case expectedType of
Type.Var' (TypeVar.Existential {}) ->
Pr.wrap "I also don't know what type it should be."
_ ->
mconcat
[ Pr.wrap "I think its type should be:",
"\n\n",
Pr.indentN 4 (style Type1 (renderType' env expectedType))
]
)
]
),
"\n\n",
Pr.hang
"Some common causes of this error include:"
( Pr.bulleted
[ Pr.wrap "Your current namespace is too deep to contain the definition in its subtree",
Pr.wrap "The definition is part of a library which hasn't been added to this project",
Pr.wrap "You have a typo in the name"
]
)
]
in mconcat
[ "I couldn't figure out what ",
style ErrorSite (Var.nameStr unknownTermV),
@ -670,32 +679,59 @@ renderTypeError e env src = case e of
[] -> undefinedSymbolHelp
wrongs -> formatWrongs wrongNameText wrongs
wrongs ->
Pr.wrap
( "The name "
<> style Identifier (Var.nameStr unknownTermV)
<> " is ambiguous. I tried to resolve it by type but"
)
<> " "
<> case expectedType of
Type.Var' (TypeVar.Existential {}) -> Pr.wrap "its type could be anything." <> "\n"
_ ->
let helpMeOut =
Pr.wrap
"no term with that name would pass typechecking. I think its type should be:"
<> "\n\n"
<> Pr.indentN 4 (style Type1 (renderType' env expectedType))
<> "\n\n"
<> Pr.wrap "If that's not what you expected, you may have a type error somewhere else in your code."
<> " "
<> Pr.wrap ("Help me out by" <> Pr.bold "using a more specific name here" <> "or" <> Pr.bold "adding a type annotation.")
<> "\n\n"
<> formatWrongs wrongTypeText wrongs
( mconcat
[ "Help me out by",
Pr.bold "using a more specific name here",
"or",
Pr.bold "adding a type annotation."
]
)
in Pr.wrap
( "The name "
<> style Identifier (Var.nameStr unknownTermV)
<> " is ambiguous. I tried to resolve it by type but"
)
<> " "
<> case expectedType of
Type.Var' (TypeVar.Existential {}) -> Pr.wrap ("its type could be anything." <> helpMeOut) <> "\n"
_ ->
mconcat
[ ( Pr.wrap $
mconcat
[ "no term with that name would pass typechecking.",
"I think its type should be:"
]
),
"\n\n",
Pr.indentN 4 (style Type1 (renderType' env expectedType)),
"\n\n",
Pr.wrap
( mconcat
[ "If that's not what you expected, you may have a type error somewhere else in your code.",
helpMeOut
]
)
]
<> "\n\n"
<> formatWrongs wrongTypeText wrongs
suggs ->
mconcat
[ "The name "
<> style Identifier (Var.nameStr unknownTermV)
<> " is ambiguous. ",
"Its type should conform to:\n\n",
Pr.indentN 4 (style Type1 (renderType' env expectedType)),
[ Pr.wrap
( mconcat
[ mconcat
[ "The name ",
style Identifier (Var.nameStr unknownTermV),
" is ambiguous. "
],
case expectedType of
Type.Var' (TypeVar.Existential {}) -> "I couldn't narrow it down by type, as any type would work here."
_ ->
"Its type should be:\n\n"
<> Pr.indentN 4 (style Type1 (renderType' env expectedType))
]
),
"\n\n",
Pr.wrap "I found some terms in scope that have matching names and types. Maybe you meant one of these:",
"\n\n",

View File

@ -310,7 +310,8 @@ Instead, it should be an unbound free variable, which doesn't typecheck:
19 | bar21
Its type should conform to _
I also don't know what type it should be.
Some common causes of this error include:
* Your current namespace is too deep to contain the
definition in its subtree
@ -366,7 +367,8 @@ The `a` introduced will be freshened to not capture the `a` in scope, so it rema
6 | a1
Its type should conform to _
I also don't know what type it should be.
Some common causes of this error include:
* Your current namespace is too deep to contain the
definition in its subtree

View File

@ -90,7 +90,10 @@ ex4 =
2 | (a,b) = (a Nat.+ b, 19)
Its type should conform to Nat
I think its type should be:
Nat
Some common causes of this error include:
* Your current namespace is too deep to contain the
definition in its subtree

View File

@ -38,7 +38,10 @@ Now, typecheck a file with a reference to `Blah.zonk` (which doesn't exist in th
2 | > Blah.zonk [1,2,3]
Its type should conform to [Nat] -> o
I think its type should be:
[Nat] -> o
Some common causes of this error include:
* Your current namespace is too deep to contain the
definition in its subtree

View File

@ -110,8 +110,9 @@ brokenDoc = {{ hello }} + 1
Doc2 -> Nat -> o
If that's not what you expected, you may have a type error
somewhere else in your code. Help me out by using a more
specific name here or adding a type annotation.
somewhere else in your code.
Help me out by using a more specific name here or adding a
type annotation.
I found some terms in scope with matching names but different
types. If one of these is what you meant, try using its full

View File

@ -116,9 +116,8 @@ useAmbiguousTerm = ambiguousTerm
1 | useAmbiguousTerm = ambiguousTerm
The name ambiguousTerm is ambiguous. Its type should conform to:
_
The name ambiguousTerm is ambiguous. I couldn't narrow it down
by type, as any type would work here.
I found some terms in scope that have matching names and
types. Maybe you meant one of these: