Opened 4 years ago

Closed 4 years ago

#11391 closed bug (fixed)

TypeError is fragile

Reported by: bgamari Owned by: diatchki
Priority: high Milestone: 8.0.1
Component: Compiler (Type checker) Version: 8.0.1-rc1
Keywords: CustomTypeErrors Cc: yav, kosmikus
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Incorrect warning at compile-time Test Case:
Blocked By: Blocking:
Related Tickets: #9637 Differential Rev(s):
Wiki Page:

Description (last modified by bgamari)

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

Change History (10)

comment:1 Changed 4 years ago by bgamari

Description: modified (diff)

comment:2 Changed 4 years ago by bgamari

Cc: kosmikus added

comment:3 Changed 4 years ago by bgamari

comment:4 Changed 4 years ago by simonpj

Keywords: CustomTypeErrors added

comment:5 Changed 4 years ago by simonpj

Owner: set to diatchki

Iavor this is you, right?

comment:6 Changed 4 years ago by diatchki

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

comment:7 Changed 4 years ago 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 likeType -> Type.

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

comment:8 Changed 4 years ago 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 <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.


>---------------------------------------------------------------

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 }

comment:9 Changed 4 years ago by Ben Gamari <ben@…>

In f0c4e46/ghc:

Add tests for #11391

comment:10 Changed 4 years ago by bgamari

Resolution: fixed
Status: newclosed

This has been merged to ghc-8.0.

Note: See TracTickets for help on using tickets.