TypeError is fragile

Consider this use of the new TypeError feature,

{-# 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,

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,

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,

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

changed milestone to %8.0.1

changed weight to 7

added Tbug Trac import typechecker labels

changed the description

Trac metadata

Trac field	Value
Related	- → #9637 (closed)

assigned to @yav

Iavor this is you, right?

That's odd, there is very explicit code that is supposed to handle these case... I'll have a look.

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 likeType -> Type.

I added a comment to userTypeError_maybe so we don't forget about this in the future.

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 6ea24af9 Author: Iavor S. Diatchki diatchki@galois.com Date: Wed Jan 13 11:30:40 2016 -0800

Handle over-applied custom type errors too.

Consider

    type family F :: Type -> Type where
       F = TypeError (Text "Error")

Now, if we see something like `F Int` we should still report the custom
type error.

---

6ea24af9 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 }

`

mentioned in commit f0c4e460

closed

This has been merged to ghc-8.0.

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedFixed

added custom type errors label

added error messages label

added Phigh label