[GHC] #11391: TypeError is fragile

[GHC]

#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