[GHC] #11391: TypeError is fragile
#11391: TypeError is fragile -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: bug | Status: new Priority: high | Milestone: 8.0.1 Component: Compiler | Version: 8.0.1-rc1 (Type checker) | Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: Incorrect Unknown/Multiple | warning at compile-time Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Consider this use of the new `TypeError` feature, {{{#!hs {-# LANGUAGE TypeInType, TypeFamilies, UndecidableInstances #-} {-# LANGUAGE UndecidableInstances #-} import Data.Kind import GHC.TypeLits (TypeError, ErrorMessage(..)) type family Resolve (t :: Type -> Type) :: Type -> Type where Resolve _ = TypeError (Text "ERROR") }}} ==== The okay case ==== Given something like, {{{#!hs testOK :: Resolve [] Int testOK = [] }}} we find that things work as expected, {{{ • ERROR • In the expression: [] :: Resolve [] Int In an equation for ‘testOK’: testOK = [] :: Resolve [] Int }}} This is what we would expect. ==== The bad case ==== However, it is very easy to fool GHC into not yielding the desired error message. For instance, {{{#!hs testNOTOK1 :: Resolve [] Int testNOTOK1 = () }}} gives us this a unification error, {{{ • Couldn't match type ‘()’ with ‘(TypeError ...)’ Expected type: Resolve [] Int Actual type: () }}} This clearly isn't what we expected. ==== The tricky case ==== Another way we can fool the typechecker is to make it attempt instance resolution on our `TypeError`, {{{#!hs testNOTOK2 :: Resolve [] Int testNOTOK2 = 1 }}} Which results in, {{{ • No instance for (Num (TypeError ...)) arising from the literal ‘1’ • In the expression: 1 In an equation for ‘testNOTOK2’: testNOTOK2 = 1 }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11391 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11391: TypeError is fragile -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: bug | Status: new Priority: high | Milestone: 8.0.1 Component: Compiler (Type | Version: 8.0.1-rc1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Description changed by bgamari: Old description:
Consider this use of the new `TypeError` feature, {{{#!hs {-# LANGUAGE TypeInType, TypeFamilies, UndecidableInstances #-} {-# LANGUAGE UndecidableInstances #-}
import Data.Kind import GHC.TypeLits (TypeError, ErrorMessage(..))
type family Resolve (t :: Type -> Type) :: Type -> Type where Resolve _ = TypeError (Text "ERROR") }}}
==== The okay case ====
Given something like, {{{#!hs testOK :: Resolve [] Int testOK = [] }}} we find that things work as expected, {{{ • ERROR • In the expression: [] :: Resolve [] Int In an equation for ‘testOK’: testOK = [] :: Resolve [] Int }}} This is what we would expect.
==== The bad case ====
However, it is very easy to fool GHC into not yielding the desired error message. For instance, {{{#!hs testNOTOK1 :: Resolve [] Int testNOTOK1 = () }}} gives us this a unification error, {{{ • Couldn't match type ‘()’ with ‘(TypeError ...)’ Expected type: Resolve [] Int Actual type: () }}} This clearly isn't what we expected.
==== The tricky case ====
Another way we can fool the typechecker is to make it attempt instance resolution on our `TypeError`, {{{#!hs testNOTOK2 :: Resolve [] Int testNOTOK2 = 1 }}} Which results in, {{{ • No instance for (Num (TypeError ...)) arising from the literal ‘1’ • In the expression: 1 In an equation for ‘testNOTOK2’: testNOTOK2 = 1 }}}
New description: Consider this use of the new `TypeError` feature, {{{#!hs {-# LANGUAGE TypeInType, TypeFamilies, UndecidableInstances #-} {-# LANGUAGE UndecidableInstances #-} import Data.Kind import GHC.TypeLits (TypeError, ErrorMessage(..)) type family Resolve (t :: Type -> Type) :: Type -> Type where Resolve _ = TypeError (Text "ERROR") }}} ==== The okay case ==== Given something like, {{{#!hs testOK :: Resolve [] Int testOK = [] }}} we find that things work as expected, {{{ • ERROR • In the expression: [] :: Resolve [] Int In an equation for ‘testOK’: testOK = [] :: Resolve [] Int }}} ==== The bad case ==== However, it is very easy to fool GHC into not yielding the desired error message. For instance, {{{#!hs testNOTOK1 :: Resolve [] Int testNOTOK1 = () }}} gives us this a unification error, {{{ • Couldn't match type ‘()’ with ‘(TypeError ...)’ Expected type: Resolve [] Int Actual type: () }}} This clearly isn't what we expected. ==== The tricky case ==== Another way we can fool the typechecker is to make it attempt instance resolution on our `TypeError`, {{{#!hs testNOTOK2 :: Resolve [] Int testNOTOK2 = 1 }}} Which results in, {{{ • No instance for (Num (TypeError ...)) arising from the literal ‘1’ • In the expression: 1 In an equation for ‘testNOTOK2’: testNOTOK2 = 1 }}} -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11391#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11391: TypeError is fragile -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: bug | Status: new Priority: high | Milestone: 8.0.1 Component: Compiler (Type | Version: 8.0.1-rc1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * cc: kosmikus (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11391#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11391: TypeError is fragile -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: bug | Status: new Priority: high | Milestone: 8.0.1 Component: Compiler (Type | Version: 8.0.1-rc1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: #9637 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * related: => #9637 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11391#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11391: TypeError is fragile -------------------------------------+------------------------------------- Reporter: bgamari | Owner: Type: bug | Status: new Priority: high | Milestone: 8.0.1 Component: Compiler (Type | Version: 8.0.1-rc1 checker) | Keywords: Resolution: | CustomTypeErrors Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: #9637 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * keywords: => CustomTypeErrors -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11391#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11391: TypeError is fragile -------------------------------------+------------------------------------- Reporter: bgamari | Owner: diatchki Type: bug | Status: new Priority: high | Milestone: 8.0.1 Component: Compiler (Type | Version: 8.0.1-rc1 checker) | Keywords: Resolution: | CustomTypeErrors Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: #9637 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * owner: => diatchki Comment: Iavor this is you, right? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11391#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11391: TypeError is fragile -------------------------------------+------------------------------------- Reporter: bgamari | Owner: diatchki Type: bug | Status: new Priority: high | Milestone: 8.0.1 Component: Compiler (Type | Version: 8.0.1-rc1 checker) | Keywords: Resolution: | CustomTypeErrors Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: #9637 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by diatchki): That's odd, there is very explicit code that is supposed to handle these case... I'll have a look. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11391#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11391: TypeError is fragile -------------------------------------+------------------------------------- Reporter: bgamari | Owner: diatchki Type: bug | Status: new Priority: high | Milestone: 8.0.1 Component: Compiler (Type | Version: 8.0.1-rc1 checker) | Keywords: Resolution: | CustomTypeErrors Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: #9637 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by diatchki): OK, it was a pretty simple fix---I just pushed the correction to master. The problem was that when I was looking for `TypeError` in a type, I forgot that it may be "over applied", because it could be used at kinds like`Type -> Type`. I added a comment to `userTypeError_maybe` so we don't forget about this in the future. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11391#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11391: TypeError is fragile
-------------------------------------+-------------------------------------
Reporter: bgamari | Owner: diatchki
Type: bug | Status: new
Priority: high | Milestone: 8.0.1
Component: Compiler (Type | Version: 8.0.1-rc1
checker) | Keywords:
Resolution: | CustomTypeErrors
Operating System: Unknown/Multiple | Architecture:
Type of failure: Incorrect | Unknown/Multiple
warning at compile-time | Test Case:
Blocked By: | Blocking:
Related Tickets: #9637 | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by simonpj):
Great work Iavor, thanks.
Always mention the ticket in the commit message! Then the ticket appears
in the Trac ticket automatically.
Also, could you add a regression test pls? (And update the "Test Case"
field of the ticket appropriately.)
Manually, the commit is
{{{
commit 6ea24af9f22f6ea661d79623135f4cd31e28c6a2
Author: Iavor S. Diatchki
---------------------------------------------------------------
6ea24af9f22f6ea661d79623135f4cd31e28c6a2 compiler/typecheck/TcRnTypes.hs | 6 +++--- compiler/types/Type.hs | 5 ++++- 2 files changed, 7 insertions(+), 4 deletions(-) diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs index 6beff7f..430a97d 100644 --- a/compiler/typecheck/TcRnTypes.hs +++ b/compiler/typecheck/TcRnTypes.hs @@ -1733,9 +1733,9 @@ isTypeHoleCt (CHoleCan { cc_hole = TypeHole }) = True isTypeHoleCt _ = False -- | The following constraints are considered to be a custom type error: --- 1. TypeError msg --- 2. TypeError msg ~ Something (and the other way around) --- 3. C (TypeError msg) (for any parameter of class constraint) +-- 1. TypeError msg a b c +-- 2. TypeError msg a b c ~ Something (and the other way around) +-- 4. C (TypeError msg a b c) (for any parameter of class constraint) getUserTypeErrorMsg :: Ct -> Maybe Type getUserTypeErrorMsg ct | Just (_,t1,t2) <- getEqPredTys_maybe ctT = oneOf [t1,t2] diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs index 6a86f70..c727da6 100644 --- a/compiler/types/Type.hs +++ b/compiler/types/Type.hs @@ -707,7 +707,10 @@ isStrLitTy _ = Nothing -- If so, give us the kind and the error message. userTypeError_maybe :: Type -> Maybe Type userTypeError_maybe t - = do { (tc, [_kind, msg]) <- splitTyConApp_maybe t + = do { (tc, _kind : msg : _) <- splitTyConApp_maybe t + -- There may be more than 2 arguments, if the type error is + -- used as a type constructor (e.g. at kind `Type -> Type`). + ; guard (tyConName tc == errorMessageTypeErrorFamName) ; return msg } }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11391#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11391: TypeError is fragile
-------------------------------------+-------------------------------------
Reporter: bgamari | Owner: diatchki
Type: bug | Status: new
Priority: high | Milestone: 8.0.1
Component: Compiler (Type | Version: 8.0.1-rc1
checker) | Keywords:
Resolution: | CustomTypeErrors
Operating System: Unknown/Multiple | Architecture:
Type of failure: Incorrect | Unknown/Multiple
warning at compile-time | Test Case:
Blocked By: | Blocking:
Related Tickets: #9637 | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Ben Gamari
#11391: TypeError is fragile -------------------------------------+------------------------------------- Reporter: bgamari | Owner: diatchki Type: bug | Status: closed Priority: high | Milestone: 8.0.1 Component: Compiler (Type | Version: 8.0.1-rc1 checker) | Keywords: Resolution: fixed | CustomTypeErrors Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: #9637 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * status: new => closed * resolution: => fixed Comment: This has been merged to `ghc-8.0`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11391#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC