Re: [GHC] #11391: TypeError is fragile

9 Jan 2016


      #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