Skip to content
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.

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

Better Custom Type Errors #278

Open
wants to merge 3 commits into
base: master
from

Conversation

@isovector
Copy link
Contributor

isovector commented Sep 26, 2019

The GHC.TypeLits.TypeError machinery is much too eager to emit TypeErrors.
This proposal loosens them up significantly so that they:

  • can produce better error messages
  • don't get in the way of more important type errors
  • aren't emitted at definition sites

Rendered

@treeowl

This comment has been minimized.

Copy link
Contributor

treeowl commented Sep 26, 2019

I haven't read through this whole thing yet, but I have also encountered the opposite problem. That is, GHC will be trying to show that a ~ MyFamily b, hit a TypeError in MyFamily b, and just tell me it can't show a ~ MyFamily b. Grrrr.... See this comment for an example.

Edit: actually, I may have stated that wrong..... I don't get the custom type error I want, but maybe I get a Coercible failure instead? I dunno. It's painful.

@phadej

This comment has been minimized.

Copy link
Contributor

phadej commented Sep 27, 2019

Any improvements with what we can do with TypeErrors are welcome.

On the other hand, I'd like the better motivations. Changing how
type-checker works should be motivated well.

TypeErrors are emitted at their definition sites, not their use sites

There are various ways to deal with an issue.
Simplest one is to

type MyErrorMessage = 'Text "This module doesn't compile"

You should also discuss relation with other unsatistifiable constraints:
To repeat

{-# LANGUAGE ConstraintKinds, GADTs, DataKinds #-}
import GHC.TypeLits
type Wrong = TypeError ('Text "err")

errors

GHCi, version 8.8.1: https://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/ogre/.ghci
[1 of 1] Compiling Main             ( TypeAlias.hs, interpreted )

TypeAlias.hs:5:1: error:
    • err
    • In the type synonym declaration for ‘Wrong’
  |
5 | type Wrong = TypeError ('Text "err")
  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

That might look inconstent, because if you do

{-# LANGUAGE ConstraintKinds, GADTs #-}

type Wrong = Int ~ Char

it doesn't error.

You can also define

foo :: Wrong => a
foo = foo

and it wont' error either. But for obvious reasons it's impossible to use
that function:

GHCi, version 8.8.1: https://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/ogre/.ghci
[1 of 1] Compiling Main             ( Equality.hs, interpreted )
Ok, one module loaded.
*Main> foo

<interactive>:1:1: error:
    • Couldn't match type ‘Int’ with ‘Char’ arising from a use of ‘foo’
    • In the expression: foo
      In an equation for ‘it’: it = foo

Yet, there's still a way to work with TypeError: type families.

{-# LANGUAGE ConstraintKinds      #-}
{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE GADTs                #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE UndecidableInstances #-}

import Data.Kind
import GHC.TypeLits

type family Wrong :: Constraint where
    Wrong = TypeError ('Text "err")

foo :: Wrong => a
foo = foo

loads into GHC nicely. And if one tries to use it, we get a TypeError:

GHCi, version 8.8.1: https://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/ogre/.ghci
[1 of 1] Compiling Main             ( TypeFamily.hs, interpreted )
Ok, one module loaded.
*Main> foo

<interactive>:1:1: error:
    • err
    • In the expression: foo
      In an equation for ‘it’: it = foo

So if you use type family you can alias TypeErrors.
I kind of understand the difference between type and type families
behaviour, but not deeply.

Default implementations

I don't understand, if I have

{-# OPTIONS_GHC -Werror=missing-methods #-}

class Foo a where
  foo :: a -> a

instance Foo Bool

errors with built-in error.

GHCi, version 8.8.1: https://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/ogre/.ghci
[1 of 1] Compiling Main             ( Class.hs, interpreted )

Class.hs:6:10: error: [-Wmissing-methods, -Werror=missing-methods]
    • No explicit implementation for
        ‘foo’
    • In the instance declaration for ‘Foo Bool’
  |
6 | instance Foo Bool
  |          ^^^^^^^^
Failed, no modules loaded.

I think that making

  • -Werror=missing-method the default behaviour
  • Somehow being able to amend built-in errors/warnings with extra hints (how to define the default implementation)

is the better way forward. Trying to tweak TypeError to do something which arguably GHC should do better itself is IMO wrong way to improve the situation.

TypeErrors get in the way of good, useful errors

The example is too complicated, does the below one highlight the issue:

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ScopedTypeVariables  #-}

import Data.Kind
import Data.Proxy
import GHC.TypeLits

type family IfOK (b :: Bool) :: Constraint where
    IfOK 'True  = ()
    IfOK 'False = TypeError ('Text "there's an error")

type AliasOfIfOK b = IfOK b

fun :: AliasOfIfOK b => Proxy b
fun = Proxy

use :: forall (b :: Bool). Proxy b
use = fun

errors with

GHCi, version 8.8.1: https://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/ogre/.ghci
[1 of 1] Compiling Main             ( Simpler.hs, interpreted )

Simpler.hs:22:7: error:
    • Could not deduce: IfOK b arising from a use of ‘fun’
    • In the expression: fun
      In an equation for ‘use’: use = fun
    • Relevant bindings include
        use :: Proxy b (bound at Simpler.hs:22:1)
   |
22 | use = fun
   |       ^^^

I'm not sure that using ErrorIfStuck hack is the right solution
to begin with.

I'm thinking that in this case when type-checker needs to satisfy
a constraint which isn't in a weak-head-normal-form, i.e
it's some unreduced type family -- and there's nothing else it can do,
there could be away to report an additional hint to built-in error,
like in previous case.

So in non-existing syntax:

type family IfOK (b :: Bool) :: Constraint where
    IfOK 'True  = ()
    IfOK 'False = TypeError ('Text "there's an error")
    {-# warn-if-stuck IfOK b = 'Text "there's another error" #-}
@treeowl

This comment has been minimized.

Copy link
Contributor

treeowl commented Sep 28, 2019

One problem I've encountered is that in many cases a type error occurs because a type is ambiguous or too polymorphic to allow a type family to reduce or an instance to be

@treeowl

This comment has been minimized.

Copy link
Contributor

treeowl commented Sep 28, 2019

One big problem I have with the current mechanism is that it gives us nothing when we can't match on the types involved, either because they're ambiguous or because they're too polymorphic. (Yes, it's sometimes possible to hack around this with overlapping instances, as @kcsongor has shown, but that has some nasty knock-on effects.) Very often, I want something a bit more in the nature of a stack trace. Vaguely speaking, I may want to register a special interest in whether a particular constraint can be resolved. Rather than just reducing it to a set of wanteds, I want to say "If you can't satisfy this constraint, I want to know explicitly."

class C m => D m
instance Q x => D (P x)

f :: ICareAbout (D m) => ...
-- or even
f :: D m `OnFailure` ('Text "Whoops! " :<>: 'ShowType m) => ...

If GHC tries to resolve D (P x) and can't satisfy Q x or C (P x) for whatever reason, I explicitly want a (possibly custom) error about D (P x).

@isovector

This comment has been minimized.

Copy link
Contributor Author

isovector commented Sep 28, 2019

Thanks for all of your feedback!

@treeowl this is definitely an idea I'm interested in. It's strongly reminiscent of @serras's WithMessage. It's a cool idea, but as the proposal points out, now you want to be able to order when those errors are emitted.

@phadej thanks for all of your input! Let me try to tackle as much of it as I can page in my brain.

There are various ways to deal with an issue.

Absolutely we can get around these things, but it's tedious and non-composable and I have yet to meet someone get any of it right on their first try. That being said, I'll make sure to point out this in the Alternatives section.

I kind of understand the difference between type and type families behavior, but not deeply.

There isn't a meaningful implementation behind this. The check as it's written is performed only as part of reportWanteds, which doesn't expand type families. For whatever reason, type synonyms hit this codepath, and type instances do not. Though as best I can tell, today's behavior is completely accidental.

Somehow being able to amend built-in errors/warnings with extra hints (how to define the default implementation)

On one hand, I agree it would be better to have more specialized machinery for this. On the other hand, -XDefaultSignatures and a well-behaving TypeError are sufficient to implement this for ourselves --- and indeed is a completely sensible implementation!

The example is too complicated

Thanks for calling this out. In the process of trying to justify it, I came up with this much simpler example:

foo :: Deferred ('Text "blah") => ()
foo = ()

-- Doesn't compile. Error message is `blah` rather than `Expected type String, but actual type ()`
bar :: String
bar = foo

I'm not sure that using ErrorIfStuck hack is the right solution to begin with.

Strongly agreed. I like your pragma idea, especially if it can be attached to any type/type synonym --- I often want to determine whether a ~ b is stuck, for example. Is your suggestion that the warn-if-stuck message is emitted whenever the constraint should be discharged, but is stuck? I'm not exactly sure what the semantics would be here, but I do like the direction.

@phadej

This comment has been minimized.

Copy link
Contributor

phadej commented Oct 1, 2019

On the other hand, -XDefaultSignatures and a well-behaving TypeError are sufficient to implement this for ourselves --- and indeed is a completely sensible implementation!

That will hide the built-in GHC error. I'm personally strongly against completely replacing compilers' built-in errors. People (and tools!) learn to recognize them.


A comparison to Deferred example is

{-# LANGUAGE GADTs #-}

foo :: Int ~ Char => ()
foo = ()

bar :: String
bar = foo

errors with

GHCi, version 8.6.5: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Main             ( Foo.hs, interpreted )

Foo.hs:7:7: error:
    • Couldn't match type ‘Int’ with ‘Char’ arising from a use of ‘foo’
    • In the expression: foo
      In an equation for ‘bar’: bar = foo
  |
7 | bar = foo
  | 

Exactly the same as with Deferred example. We get Int is not Char -error. Not String is not ().


Yet

foo :: Ord a => a -> String
foo _ = 42

bar :: ()
bar = foo (succ :: Bool -> Bool)

with

    • Couldn't match type ‘[Char]’ with ‘()’
      Expected type: ()
        Actual type: String
    • In the expression: foo (succ :: Bool -> Bool)
      In an equation for ‘bar’: bar = foo (succ :: Bool -> Bool)
  |
5 | bar = foo (succ :: Bool -> Bool)
  |

and not with

 No instance for (Ord (Bool -> Bool)) arising from a use of ‘foo’

I hope that there would be a good story, so I as library writer could understand which type errors will happens when. E.g. if I rewrite Member in original proposal to be a class, will things work as expected (i.e. only when GHC decides to pursue finding the Member instance it will run into TypeError?)


My current intuition is that TypeError is error on type-level, so when GHC while evaluating types tries to seq the TypeError it will fail. Is this correct, or not? How more dependent stuff will change that?


Is your suggestion that the warn-if-stuck message is emitted whenever the constraint should be discharged, but is stuck? I'm not exactly sure what the semantics would be here, but I do like the direction.

I have very operational feeling to it only. When the type-checker is searching for an instance or type-equality, and the operand is type-family application: then in addition to reporting Cannot satisfy IsOK b or Couldn't match Foo a with 'True, GHC could report something extra.

@tydeu

This comment has been minimized.

Copy link

tydeu commented Oct 2, 2019

From the proposal:

Do we really need to worry about the backwards compatibility changes in Part 1.5? Things would be drastically simpler without them.

Yes, please worry about this. I use TypeError often in my type family heavy code to provide helpful errors when the family isn't used properly, so I would very much like to keep that functionality. Otherwise it would be very hard to know what went wrong when a type family does not reduce as expected.

In general, though, I like this proposal. It would be very useful to be able to define types synynoms of type errors. My current approach has been to use TemplateHaskell, but that is kind of overkill.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
4 participants
You can’t perform that action at this time.