[GHC] #14771: TypeError reported too eagerly
#14771: TypeError reported too eagerly -------------------------------------+------------------------------------- Reporter: hsyl20 | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.2 (Type checker) | Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: Incorrect Unknown/Multiple | error/warning at compile-time Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Consider the following example: {{{#!hs {-# 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14771 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14771: TypeError reported too eagerly -------------------------------------+------------------------------------- Reporter: hsyl20 | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.2 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple error/warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * cc: diatchki (added) Comment: Iavor, ideas? `TypeError` is your baby -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14771#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14771: TypeError reported too eagerly -------------------------------------+------------------------------------- Reporter: hsyl20 | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.2 checker) | Keywords: Resolution: | CustomTypeErrors Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple error/warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * keywords: => CustomTypeErrors -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14771#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14771: TypeError reported too eagerly -------------------------------------+------------------------------------- Reporter: hsyl20 | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.2 checker) | Keywords: Resolution: | CustomTypeErrors Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple error/warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14771#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
I guess a better solution, although more complex, would be too look at
#14771: TypeError reported too eagerly -------------------------------------+------------------------------------- Reporter: hsyl20 | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.2 checker) | Keywords: Resolution: | CustomTypeErrors Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple error/warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by hsyl20): 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`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14771#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14771: TypeError reported too eagerly -------------------------------------+------------------------------------- Reporter: hsyl20 | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.2 checker) | Keywords: Resolution: | CustomTypeErrors Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple error/warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14771#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14771: TypeError reported too eagerly -------------------------------------+------------------------------------- Reporter: hsyl20 | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.2 checker) | Keywords: Resolution: | CustomTypeErrors Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple error/warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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") }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14771#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14771: TypeError reported too eagerly -------------------------------------+------------------------------------- Reporter: hsyl20 | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.2 checker) | Keywords: Resolution: | CustomTypeErrors Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple error/warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14771#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC