Opened 20 months ago

Last modified 20 months ago

#14771 new bug

TypeError reported too eagerly

Reported by: hsyl20 Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 8.2.2
Keywords: CustomTypeErrors Cc: diatchki
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Incorrect error/warning at compile-time Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

Consider the following example:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}

import GHC.TypeLits
import Data.Proxy

data DUMMY

type family If c t e where
   If True t e  = t
   If False t e = e


type family F (n :: Nat) where
   --F n = If (n <=? 8) Int (TypeError (Text "ERROR"))
   F n = If (n <=? 8) Int DUMMY

test :: (F n ~ Word) => Proxy n -> Int
test _ = 2

test2 :: Proxy (n :: Nat) -> Int
test2 p = test p

main :: IO ()
main = do
   print (test2 (Proxy :: Proxy 5))

The type error is useful:

Bug.hs:26:11: error:
    • Couldn't match type ‘If (n <=? 8) Int DUMMY’ with ‘Word’
        arising from a use of ‘test’
    • In the expression: test p
      In an equation for ‘test2’: test2 p = test p
    • Relevant bindings include
        p :: Proxy n (bound at Bug.hs:26:7)
        test2 :: Proxy n -> Int (bound at Bug.hs:26:1)
   |
26 | test2 p = test p
   |           ^^^^^^

Now if we use the commented implementation of F (using TypeError), with GHC 8.2.2 and 8.0.2 we get:

Bug.hs:26:11: error:
    • ERROR
    • In the expression: test p
      In an equation for ‘test2’: test2 p = test p
   |
26 | test2 p = test p
   |           ^^^^^^

While with GHC 8.0.1 we get:

/home/hsyl20/tmp/Bug.hs:29:11: error:
    • Couldn't match type ‘If (n <=? 8) Int (TypeError ...)’
                     with ‘Word’
        arising from a use of ‘test’
    • In the expression: test p
      In an equation for ‘test2’: test2 p = test p

1) Could we restore the behavior of GHC 8.0.1?

2) In my real code, when I use DUMMY I get:

    • Couldn't match type ‘If (n <=? 8) Int8 DUMMY’ with ‘Word’
      Expected type: Word
        Actual type: F n

If we could get the same report (mentioning the "Actual type") when we use TypeError that would be great.

Change History (7)

comment:1 Changed 20 months ago by simonpj

Cc: diatchki added

Iavor, ideas? TypeError is your baby

comment:2 Changed 20 months ago by simonpj

Keywords: CustomTypeErrors added

comment:3 Changed 20 months ago by diatchki

For issue 1:

the high-level question is what to do when we encounter an unevaluated type function with an error parameter (e.g., T x (TypeError ...)). Currently, we always report such errors, which is simple, but probably too eager in some cases.

I guess a better solution, although more complex, would be too look at the available equations for T and see if evaluation is "stuck" due to the type error. If so, we report the custom error. Otherwise, we leave the expression as is. Note, however, that if we choose to not report the custom error we'd get a rather ugly "normal" error, as GHC would still print the description of the error (in combinator form) when it is rendering the type.

For issue 2: I am not sure I understand 100% what the request is. Could you give a concrete example?

comment:4 Changed 20 months ago by hsyl20

I guess a better solution, although more complex, would be too look at the available equations for T and see if evaluation is "stuck" due to the type error. If so, we report the custom error. Otherwise, we leave the expression as is.

That would be good!


Regarding the issue 2: say GHC can't solve F n ~ Word as in the given example. Currently it reports:

    • Couldn't match type ‘If (n <=? 8) Int DUMMY’ with ‘Word’

Sometime in other places in my code (I don't know how to reproduce it in the smaller example) it reports the following, which is better because it mentions F n:

    • Couldn't match type ‘If (n <=? 8) Int8 DUMMY’ with ‘Word’
      Expected type: Word
        Actual type: F n

I'd like F n to appear more often instead of having to remember that the complex expression If (n <=? 8) ... refers to F n. Maybe we could even suggest adding F n ~ Word as a constraint for test2.

comment:5 Changed 20 months ago by diatchki

Ok, so I think issue 2) is not related to custom type errors. I haven't looked at this part of the error reporting much, but I suspect that in some cases GHC forgets that some type expression is the result of evaluating a function. Tricky business. I'd say it'd be better to file a separate ticket for this, especially if you can find a concrete example that might point out to exactly what we may fix.

comment:6 Changed 20 months ago by diatchki

As for issue 1), I am a bit weary of doing the change, as the current behavior has a fairly simple explanation; the alternative I mentioned would be more of a heuristic, as I don't think we have a specific order of evaluation, and it could make some custom errors not show up, when you'd like them to show.

Generally, even though TypeError is implemented just as a type function, I really think of it more of a special right-hand side in type function definitions. If you use it in this way, then you don't encounter the problems you found, because the type error is only ever generated when there is no other alternative. So this is how I'd structure your example in this style:

type family Assert (prop :: Bool) (val :: k) (msg :: ErrorMessage) where
   Assert 'True  val msg = val
   Assert 'False val msg = TypeError msg

In fact, we should probably add this type function to Data.Type.Bool.

With this combinator, you could define F simply as:

type F n = Assert (n <=? 8) Int (Text "Input to F should be no greater than 8")

comment:7 Changed 20 months ago by hsyl20

Nice! Assert did the trick, thanks!

I'll fill another ticket for issue 2 if I find a better example.

I leave the ticket open to discuss if we want Assert to be added to Data.Type.Bool. Otherwise we can close it.

Note: See TracTickets for help on using tickets.