[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       |           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