Skip to content

Add support polykind for Quote from Prim.TypeError #4142

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

Merged
rhendric merged 3 commits into from
Nov 17, 2021
Merged

Add support polykind for Quote from Prim.TypeError #4142

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
be98777
Make `Quote` from `Prim.TypeError` polykinded
xgrommx Jul 8, 2021
3f2001d
Merge remote-tracking branch 'upstream/master' into fix-type-error-quote
JordanMartinez Nov 16, 2021
8870619
Add changelog entry
JordanMartinez Nov 16, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions CHANGELOG.d/feature_make-quote-work-on-more-kinds.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
* Make `Prim.TypeError`'s `Quote` work on all kinds, not just kind `Type`.
1 change: 1 addition & 0 deletions CONTRIBUTORS.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -149,6 +149,7 @@ If you would prefer to use different terms, please use the section below instead
| [@mhmdanas](https://github.com/mhmdanas) | Mohammed Anas | [MIT license](http://opensource.org/licenses/MIT) |
| [@kl0tl](https://github.com/kl0tl) | Cyril Sobierajewicz | [MIT license](http://opensource.org/licenses/MIT) |
| [@PureFunctor](https://github.com/PureFunctor) | Justin Garcia | [MIT license](http://opensource.org/licenses/MIT) |
| [@xgrommx](https://github.com/xgrommx) | Denis Stoyanov | [MIT license](http://opensource.org/licenses/MIT) |

### Contributors using Modified Terms

Expand Down
2 changes: 1 addition & 1 deletion lib/purescript-cst/src/Language/PureScript/Environment.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -429,7 +429,7 @@ primTypeErrorTypes =
, (primSubName C.typeError "Fail", (kindDoc -:> kindConstraint, ExternData [Nominal]))
, (primSubName C.typeError "Warn", (kindDoc -:> kindConstraint, ExternData [Nominal]))
, (primSubName C.typeError "Text", (kindSymbol -:> kindDoc, ExternData [Phantom]))
, (primSubName C.typeError "Quote", (kindType -:> kindDoc, ExternData [Phantom]))
, (primSubName C.typeError "Quote", (tyForall "k" kindType $ tyVar "k" -:> kindDoc, ExternData [Phantom]))
, (primSubName C.typeError "QuoteLabel", (kindSymbol -:> kindDoc, ExternData [Phantom]))
, (primSubName C.typeError "Beside", (kindDoc -:> kindDoc -:> kindDoc, ExternData [Phantom, Phantom]))
, (primSubName C.typeError "Above", (kindDoc -:> kindDoc -:> kindDoc, ExternData [Phantom, Phantom]))
Expand Down
2 changes: 1 addition & 1 deletion src/Language/PureScript/Errors.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1861,7 +1861,7 @@ toTypelevelString (TypeLevelString _ s) =
Just . Box.text $ decodeStringWithReplacement s
toTypelevelString (TypeApp _ (TypeConstructor _ f) x)
| f == primSubName C.typeError "Text" = toTypelevelString x
toTypelevelString (TypeApp _ (TypeConstructor _ f) x)
toTypelevelString (TypeApp _ (KindApp _ (TypeConstructor _ f) _) x)
| f == primSubName C.typeError "Quote" = Just (typeAsBox maxBound x)
toTypelevelString (TypeApp _ (TypeConstructor _ f) (TypeLevelString _ x))
| f == primSubName C.typeError "QuoteLabel" = Just . line . prettyPrintLabel . Label $ x
Expand Down
18 changes: 18 additions & 0 deletions tests/purs/failing/ProgrammablePolykindedTypeErrorsTypeString.out
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
Error found:
in module Main
at tests/purs/failing/ProgrammablePolykindedTypeErrorsTypeString.purs:23:7 - 23:17 (line 23, column 7 - line 23, column 17)

A custom type error occurred while solving type class constraints:

Don't want to show Just @Type String because.
Copy link
Copy Markdown
Contributor

@hdgarrood hdgarrood Jul 9, 2021 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think we should probably strip the kind annotations out here (the @Type bit).

Copy link
Copy Markdown
Member

@rhendric rhendric Jul 9, 2021

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We still want to show them when --verbose-errors is set, right?

Copy link
Copy Markdown
Contributor

@hdgarrood hdgarrood Jul 9, 2021

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If we already decided on a strategy of showing kind annotations when verbose errors is on, then applying that same strategy here sounds good. I can’t remember whether that should be happening anyway; do the tests run with verbose errors on?

Copy link
Copy Markdown
Member

@rhendric rhendric Jul 9, 2021

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

As far as I can tell, in the only places we're currently erasing kind annotations in error messages, we do so conditional on verbose errors being off. I believe the tests don't run with verbose errors, which maybe makes testing that the erasure is conditional on verbosity difficult.

Also, it seems there are plenty of other places where we don't do this and perhaps should (just grep for @ in tests/**/*.out), which maybe makes dumping this request on this PR a little unfair? I agree that it should be done, but maybe we should clean this up holistically (and figure out how to test it robustly) in a separate PR.

Copy link
Copy Markdown
Contributor

@hdgarrood hdgarrood Jul 9, 2021

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ok, yes, that makes sense.

Copy link
Copy Markdown
Contributor

@natefaubion natefaubion Jul 9, 2021

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We don’t strip them in the error “trace” to aid debugging.



while checking that type Fail (Beside (Beside (Text "Don\'t want to show ") (... ...)) (Text " because.")) => String
is at least as general as type String
while checking that expression someString
has type String
in value declaration main

See https://github.com/purescript/documentation/blob/master/errors/NoInstanceFound.md for more information,
or to contribute content related to this error.

23 changes: 23 additions & 0 deletions tests/purs/failing/ProgrammablePolykindedTypeErrorsTypeString.purs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,23 @@
-- @shouldFailWith NoInstanceFound

module Main where

import Prelude
import Prim.TypeError
import Effect (Effect)
import Effect.Console (log)

data Maybe :: forall k. k -> Type
data Maybe a

foreign import data Nothing :: forall k. Maybe k
foreign import data Just :: forall k. k -> Maybe k

someString :: Fail (Text "Don't want to show " <> Quote (Just String) <> Text " because.") => String
someString = "someString"

infixl 6 type Beside as <>

main :: Effect Unit
main = do
log someString