Opened 10 years ago

Closed 4 years ago

Last modified 4 years ago

#1496 closed bug (fixed)

Newtypes and type families combine to produce inconsistent FC(X) axiom sets

Reported by: sorear Owned by: simonpj
Priority: normal Milestone: 7.6.2
Component: Compiler (Type checker) Version: 6.7
Keywords: Cc: samb, chak@…, ganesh.sittampalam@…, lennart.augustsson@…, tom.schrijvers@…, df@…, mjm2002@…, pumpkingod@…, ben@…, jmaessen@…, hackage.haskell.org@…, ezyang@…
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: deriving/should_fail/T1496
Blocked By: Blocking: #5498
Related Tickets: Differential Rev(s):
Wiki Page:

Description (last modified by sorear)

Given:

{-# OPTIONS_GHC -ftype-families #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
data family Z :: * -> *

newtype Moo = Moo Int

newtype instance Z Int = ZI Double
newtype instance Z Moo = ZM (Int,Int)

We generate the axioms:

(from the instances)
Z Int ~ Double
Z Moo ~ (Int,Int)

(from the newtype)
Moo ~ Int

And can prove:

(production REFL in the FC(X) paper)
Z ~ Z

(production COMP)
Z Moo ~ Z Int

(production TRANS)
Z Moo ~ Double

(production SYM)
Double ~ Z Moo

(production TRANS)
Double ~ (Int,Int)

Tickling this seems to require the newtype cheat, but the inconsistant axioms allow code to pass Core Lint and still crash:

newtype Moo = Moo Int deriving(IsInt)
class IsInt t where
    isInt :: c Int -> c t
instance IsInt Int where isInt = id
main = case isInt (ZI 4.0) of ZM tu -> print tu
stefan@stefans:/tmp$ ghc -dcore-lint Z.hs
stefan@stefans:/tmp$ ./a.out
Segmentation fault
stefan@stefans:/tmp$ ghc -V
The Glorious Glasgow Haskell Compilation System, version 6.7.20070612
stefan@stefans:/tmp$

Change History (45)

comment:1 Changed 10 years ago by sorear

Component: CompilerCompiler (Type checker)
Description: modified (diff)
Summary: System FC{Newtypes,TypeFamilies} is unsoundNewtypes and type families combine to produce inconsistent FC(X) axiom sets

comment:2 Changed 10 years ago by SamB

severity: normalcritical

An unsound typesystem is a very bad thing.

comment:3 Changed 10 years ago by SamB

Cc: samb added

comment:4 Changed 10 years ago by chak

Cc: chak added

There are really two issues here mixed up. One one hand we have an infelicity in combining the FC equalities introduced by newtypes and type families. That's a bad thing from a theoretical point of view, but I don't know of an exploit to break type safety with that. In fact, I think it is merely a problem of the type-preserving translation to FC in GHC and not with the source type system (ie, all accepted programs are fine, even if they lead to fishy FC).

On the other hand, the example code demonstrates that newtype deriving in its current generality is unsound and leads GHC to accept source programs that it should not accept. Here is an alternative example that exploits the same problem using GADTs instead of type families (its not quite as dramatic as it doesn't segv, but it refutes an irrefutable pattern it really shouldn't):

{-# LANGUAGE GeneralizedNewtypeDeriving #-}

class IsInt t where
    isInt :: c Int -> c t
instance IsInt Int where isInt = id

newtype Moo = Moo Int deriving(IsInt,Show)

data Z a where
  ZI :: Double -> Z Int
  ZM :: (Int, Int) -> Z Moo

foo :: Z Moo -> Moo
foo ~(ZM (i, _)) = Moo i

main = print $ foo (isInt (ZI 4.0))

comment:5 Changed 10 years ago by sorear

As I see it, the fundamental issue here is that the treatment of newtypes is inconsistent between Haskell and Core. In Haskell, newtypes are just cheap data, and they can only be added or removed at the top level of a type. In FC(X), newtypes are rather more like type level lambdas, and can be added or removed anywhere in a type expression as long as the points where β-conversion occurs are clearly marked with cast.

The introduction of generalized newtype deriving complicated this. Because you can use the newtype function on an arbitrary dictionary, you can construct any value, including Leibniz equality witnesses, thus allowing FC(X)'s newtype semantics to escape into the Haskell world.

Many other language features, such as GADTs, associated types, and (I strongly suspect, but have not been able to prove due to the difficulty inherent in comprehending them) functional dependencies, were implemented so as to deeply assume Haskell-98 newtype semantics, and break when exposed to FC(X) lambda semantics.

So, there are two options.

  1. Make Haskell look like FC(X)

We would need to treat newtypes as fully transparent for the purposes of overlap checks in associated-type and fundep checking, and for GADT overlap/inaccessibility checking.

  1. Make FC(X) look like Haskell

We could add a new kind constructor NCO. (Using the concrete syntax of the Calculus of Constructions, with *{0} the sort of values and *{1} the sort of types, eg Bool : *{0} : *{1}):

NCO : [kind : *{1}] [lty : kind] [rty : kind] *{0}

Then, we can generalize TRANS and SYM to work on NCO: (in practice we'd use ad-hoc polymorphism)

TRANS_n : [kind : *{1}] [t1 : kind] [t2 : kind] [t3 : kind] [lco : NCO kind t1 t2] [rco : NCO kind t2 t3] NCO kind t1 t3 SYM_n : [kind : *{1}] [t1 : kind] [t2 : kind] [co : NCO kind t1 t2] NCO kind t2 t1

A subtyping relation exists:

SUB : [kind : *{1}] [t1 : kind] [t2 : kind] [co : CO kind t1 t2] NCO kind t1 t2

and REFL, CAST use NCO; while (this is very important) COMP, LEFT, and RIGHT continue to use full CO's. Thus a NCO represents a coercion that is only valid at the top level because it cannot be composed, and this restriction is enforced by Core Lint. (Perhaps it would be good to make other kinds of type function use NCO?)

comment:6 Changed 10 years ago by guest

Cc: ganesh.sittampalam@… added

comment:7 Changed 10 years ago by chak

Cc: chak@… added; chak removed

For completenes sake, please not that this bug is related to #1251, as was pointed out on #haskell.

comment:8 Changed 10 years ago by chak

Also note the type of the newtype-derived

isInt :: c Int -> c Moo

Parametricity laws for higher-kinded variables are tricky, but if I am not mistaken, this type should not be inhabited by any terminating functions - that is, on the level of the source type system. After all, the newtype declaration promises to introduce a new type dinstinct from all others.

As SimonPJ notes in Bug #1251, newtype deriving lifts the newtype coercion CoMoo to the source type level and that is IMHO the cause of the problem, as it violates the intention of newtype.

comment:9 Changed 10 years ago by guest

Cc: lennart.augustsson@… added

Newtype deriving the way it's done in ghc is scary. I think a newtype deriving should only be allowed if you (i.e., the compiler) can actually construct the instance declaration. This might be less general, but it would make me much more confident that it's correct.

comment:10 Changed 10 years ago by SamB

Yeah, I also think that GHC should insist on being able to find an instance declaration -- though I don't care what it does with said declaration afterwards ;-).

comment:11 Changed 10 years ago by igloo

Milestone: 6.8
Owner: set to simonpj
Priority: normalhigh

comment:12 Changed 10 years ago by toms

Cc: tom.schrijvers@… added

There are two issues here.

1) The newtype coercions are not sound. They are unsafe and only to be used in disciplined ways.

The type Moo is different from the type Int. Hence, we shouldn't mix up values of both types. With the newtype coercion Moo ~ Int, there exists the danger that we would: a malicious or erroneous Core transformation may do so without being exposed by ill-typing. Hence, Core is less strongly typed than Haskell source. At present, there does not seem to be a satisfactory way to encode newtypes in Core that both preserves the strong typing and the optimizations.

Simon points out that other unsafe coercions are also created, e.g. the expression

   case error @ Int "bla" of _ -> 'z'

is transformed into

   error @ Int "blah" `cast` (co :: Int ~ Char)

where Int~Char is clearly unsound.

2) The newtype deriving construct is an undisciplined use of newtype coercions that exposes their unsafety.

The unsound assumption made is that every higher-order type that is applied to the newtype is an algebraic functor (not explicitly required to be an instance of the typeclass Functor).

For the isInt newtype deriving this could be written as:

instance IsInt Moo where
  isInt x = fmap (`cast` (co :: Int ~ Moo)) . (isInt :: c Int -> c Int)

Using the 'fmap cast' lifting law:

fmap (`cast` (co :: Int ~ Moo)) == (`cast` (c co :: c Int ~ c Moo))

we get:

instance IsInt Moo where
  isInt x = (`cast` (c co :: c Int ~ c Moo)) . (isInt :: c Int -> c Int)

which is what the newtype deriving actually generates straight away, without checking whether c is a functor, whether fmap and the lifting law are at all applicable.

It seems that vanilla algebraic datatypes that are polymorphic, are implict functors. And it's this those implicit instances that are used by the newtype deriving.

However, GADTs are definitely not functors. Some shapes of values can only be used for certain types, regardless of whether any values of that type are involved at all, e.g. the ZI constructor can only be used for Int and not for Moo. Data families are essentially open GADTs.

We can attempt to fix the situation by imposing conditions on the types involved in a newtype deriving:

  • generate the fmap code, and hence demand explicit Functor instances. We should be able to expect the compiler to eliminate any runtime overhead.
  • conservatively check that only well-behaved higher-order types are applied to the newtype: this rules out GADTs, data & type families, type variables (which can be instantiated with ill-behaved types), but also ordinary ADTs that hide ill-behaved types, like data T a = MkT (GADT a).

The second option seems to be too complicated to be reasonable and the first option perhaps too clumsy to be useful. The least I would do is to deprecate the use of newtype deriving.

comment:13 Changed 10 years ago by guest

Cc: kfrdbs@… added

comment:14 in reply to:  12 Changed 10 years ago by Isaac Dupree

Replying to toms:

However, GADTs are definitely not functors.

...

We can attempt to fix the situation by imposing conditions on the types involved in a newtype deriving:

  • generate the fmap code, and hence demand explicit Functor instances. We should be able to expect the compiler to eliminate any runtime overhead.

From Frisby we have a data type that is a Functor and a GADT, but not a Functor in the way you and GHC expect:

data PE a where
-- leaving out most of the constructors, but note especially PMap
    Char :: IntSet.IntSet -> PE Char
    Failure :: PE a
    Not :: PE a -> PE ()
    Then :: PE a -> PE b -> PE (a,b)
    PMap :: (a -> b) -> PE a -> PE b

instance Functor PE where
    fmap = PMap

Applying the fmap-option would make interesting, type-correct code be generated that could not be optimized away (so the dictionaries couldn't be shared).

comment:15 Changed 10 years ago by simonmar

Milestone: 6.8 branch6.10 branch
Priority: highnormal

comment:16 Changed 10 years ago by dfranke

Cc: df@… added; kfrdbs@… removed

comment:17 Changed 9 years ago by simonmar

Architecture: UnknownUnknown/Multiple

comment:18 Changed 9 years ago by simonmar

Operating System: UnknownUnknown/Multiple

comment:19 Changed 9 years ago by morrow

Cc: mjm2002@… added

comment:20 Changed 9 years ago by simonpj

See #2721 for another example.

comment:21 Changed 8 years ago by igloo

Milestone: 6.10 branch6.12 branch

comment:22 Changed 8 years ago by SamB

Okay, it seems to me that in order to solve this problem, GHC needs to be able to prove, somehow or other, that each method to be derived can be safely converted from the one type to the other. Correct?

And the main choice here is whether it should

  1. try to do this on it's own, and prove that it can just cast between the one and the other or
  2. require the user to explicitly provide Functor, BiFunctor, etc. instances for GHC to use during this process,

yes?

Probably it is best to take an approach that we can be sure is safe without too many aspirins, and use approach B, but have GHC issue a warning whenever it is unable to optimize away the coercions for some of the methods, and therefore unable to re-use the dictionary.

The rules for the derivation itself should preferably be written up in a paper so that the other compilers, too, can benefit from this extremely convenient feature, though doubtless it will become somewhat less convenient in some ways if this bug is fixed.

For this approach to work well with multi-parameter types, however, we'd presumably need to add a lot more Functor-related classes to base, would we not?

But which ones?

comment:23 Changed 8 years ago by SamB

Well, we had a conversation about this on IRC today, and Cale has convinced me that there is a bug in the definition of ~ in your papers.

<Cale> The main reason that newtypes exist is 1) to ensure that things are not confused with the original type, and 2) to allow separate instances to be written without overhead.
<Cale> For ~ to resolve them as the same type goes against both.
<Cale> Basically, the way that ~ is treating newtype right now is how it ought to be treating 'type'

comment:24 Changed 8 years ago by pumpkin

Cc: pumpkingod@… added

comment:25 Changed 8 years ago by BenMoseley

Cc: ben@… added

comment:26 Changed 7 years ago by jmaessen

Cc: jmaessen@… added
Type of failure: None/Unknown

Here's a simple example program that violates the invariant of Set while using only newtype deriving (and not more complex extensions such as multiparameter type classes or type functions):

{-# LANGUAGE GeneralizedNewtypeDeriving #-}
module Main(main) where
import Data.Set

class IsoInt a where
    convFromInt :: item Int -> item a

instance IsoInt Int where
    convFromInt = id

newtype Down a = Down a deriving (Eq, Show, IsoInt)

instance Ord a => Ord (Down a) where
    compare (Down a) (Down b) = compare b a

asSetDown :: Set (Down Int) -> Set (Down Int)
asSetDown = id

a1 = toAscList . asSetDown . convFromInt . fromAscList $  [0..10]
a2 = toAscList . asSetDown . fromAscList . reverse . convFromInt $ [0..10]

main = do
    print a1
    print a2

comment:27 Changed 7 years ago by igloo

Milestone: 6.12 branch6.12.3

comment:28 Changed 7 years ago by igloo

Milestone: 6.12.36.14.1
Priority: normallow

comment:29 Changed 7 years ago by simonpj

See also #4846

comment:30 Changed 7 years ago by igloo

Milestone: 7.0.17.0.2

comment:31 Changed 6 years ago by igloo

Milestone: 7.0.27.2.1

comment:32 Changed 6 years ago by liyang

Cc: hackage.haskell.org@… added

comment:33 Changed 6 years ago by igloo

Milestone: 7.2.17.4.1

comment:34 Changed 6 years ago by simonpj

See also #5498

comment:35 Changed 6 years ago by simonpj

Blocking: 5498 added

comment:36 Changed 5 years ago by igloo

Milestone: 7.4.17.6.1
Priority: lownormal

comment:37 Changed 5 years ago by ezyang

Cc: ezyang@… added

comment:38 Changed 5 years ago by simonpj

See also #7148

comment:39 Changed 5 years ago by igloo

Milestone: 7.6.17.6.2

comment:40 Changed 5 years ago by morabbin

Is this bug handled by the POPL 2011 paper "Generative Type Abstraction and Type-level Computation"? Noted in #4846 as pointing the way to solving the problems therein.

comment:41 Changed 4 years ago by simonpj

See also How GADTs inhibit abstraction. I have not studied it closely but it's clearly relevant.

comment:42 Changed 4 years ago by goldfire

See Roles for the concrete approach toward a solution. Expect a working implementation to be available within a week or two.

comment:43 Changed 4 years ago by eir@…

commit e8aa8ccba0c40884765281b21ff8f4411802dd41

Author: Richard Eisenberg <eir@cis.upenn.edu>
Date:   Fri Aug 2 15:47:03 2013 +0100

    Implement "roles" into GHC.
    
    Roles are a solution to the GeneralizedNewtypeDeriving type-safety
    problem.
    
    Roles were first described in the "Generative type abstraction" paper,
    by Stephanie Weirich, Dimitrios Vytiniotis, Simon PJ, and Steve Zdancewic.
    The implementation is a little different than that paper. For a quick
    primer, check out Note [Roles] in Coercion. Also see
    http://ghc.haskell.org/trac/ghc/wiki/Roles
    and
    http://ghc.haskell.org/trac/ghc/wiki/RolesImplementation
    For a more formal treatment, check out docs/core-spec/core-spec.pdf.
    
    This fixes Trac #1496, #4846, #7148.

 compiler/basicTypes/DataCon.lhs                   |   10 +-
 compiler/basicTypes/MkId.lhs                      |   14 +-
 compiler/cmm/SMRep.lhs                            |   42 +-
 compiler/coreSyn/CoreLint.lhs                     |  123 ++--
 compiler/coreSyn/CoreSubst.lhs                    |    8 +-
 compiler/coreSyn/CoreUtils.lhs                    |   16 +-
 compiler/coreSyn/ExternalCore.lhs                 |   29 +-
 compiler/coreSyn/MkExternalCore.lhs               |   24 +-
 compiler/coreSyn/PprExternalCore.lhs              |   60 +-
 compiler/coreSyn/TrieMap.lhs                      |   82 ++-
 compiler/deSugar/DsBinds.lhs                      |   59 +-
 compiler/deSugar/DsForeign.lhs                    |    2 +-
 compiler/deSugar/DsMeta.hs                        |  106 ++-
 compiler/ghci/ByteCodeAsm.lhs                     |   16 +-
 compiler/hsSyn/Convert.lhs                        |   19 +-
 compiler/hsSyn/HsTypes.lhs                        |   25 +-
 compiler/hsSyn/HsUtils.lhs                        |    2 +-
 compiler/iface/BinIface.hs                        |    1 +
 compiler/iface/BuildTyCl.lhs                      |   43 +-
 compiler/iface/IfaceSyn.lhs                       |  128 ++--
 compiler/iface/IfaceType.lhs                      |  343 ++++++---
 compiler/iface/MkIface.lhs                        |   19 +-
 compiler/iface/TcIface.lhs                        |   75 +-
 compiler/main/DynFlags.hs                         |    2 +
 compiler/parser/Lexer.x                           |   31 +-
 compiler/parser/Parser.y.pp                       |   26 +-
 compiler/parser/ParserCore.y                      |    7 +-
 compiler/parser/RdrHsSyn.lhs                      |    8 +-
 compiler/prelude/PrelNames.lhs                    |    4 +-
 compiler/prelude/PrelRules.lhs                    |    4 +-
 compiler/prelude/TysPrim.lhs                      |   62 +-
 compiler/prelude/TysWiredIn.lhs                   |    4 +
 compiler/rename/RnTypes.lhs                       |   43 +-
 compiler/simplCore/SimplUtils.lhs                 |    2 +-
 compiler/specialise/Rules.lhs                     |    7 +-
 compiler/specialise/SpecConstr.lhs                |    2 +-
 compiler/stranal/WwLib.lhs                        |    4 +-
 compiler/typecheck/TcDeriv.lhs                    |   16 +-
 compiler/typecheck/TcEvidence.lhs                 |    8 +-
 compiler/typecheck/TcForeign.lhs                  |   48 +-
 compiler/typecheck/TcGenGenerics.lhs              |    2 +-
 compiler/typecheck/TcHsType.lhs                   |  105 ++-
 compiler/typecheck/TcInstDcls.lhs                 |   13 +-
 compiler/typecheck/TcInteract.lhs                 |    3 +-
 compiler/typecheck/TcRnDriver.lhs                 |   12 +-
 compiler/typecheck/TcSplice.lhs                   |   42 +-
 compiler/typecheck/TcTyClsDecls.lhs               |  302 ++++++--
 compiler/typecheck/TcTyDecls.lhs                  |  293 +++++++-
 compiler/typecheck/TcType.lhs                     |    7 +-
 compiler/types/Class.lhs                          |    6 +-
 compiler/types/CoAxiom.lhs                        |   82 ++-
 compiler/types/Coercion.lhs                       |  802 +++++++++++++++------
 compiler/types/FamInstEnv.lhs                     |   78 +-
 compiler/types/OptCoercion.lhs                    |  199 +++--
 compiler/types/TyCon.lhs                          |  110 ++-
 compiler/types/Type.lhs                           |    9 +-
 compiler/types/TypeRep.lhs                        |    2 +-
 compiler/utils/Maybes.lhs                         |    5 +
 compiler/utils/UniqFM.lhs                         |    2 +-
 compiler/utils/Util.lhs                           |   10 +-
 compiler/vectorise/Vectorise/Generic/PAMethods.hs |    8 +-
 compiler/vectorise/Vectorise/Generic/PData.hs     |    1 +
 compiler/vectorise/Vectorise/Type/Env.hs          |    2 +-
 compiler/vectorise/Vectorise/Type/TyConDecl.hs    |    2 +
 compiler/vectorise/Vectorise/Utils/Base.hs        |    4 +-
 compiler/vectorise/Vectorise/Utils/PADict.hs      |    2 +-
 docs/core-spec/CoreLint.ott                       |  178 +++--
 docs/core-spec/CoreSyn.ott                        |   77 +-
 docs/core-spec/OpSem.ott                          |    2 +-
 docs/core-spec/README                             |    2 +-
 docs/core-spec/core-spec.mng                      |   54 +-
 docs/core-spec/core-spec.pdf                      |  Bin 349150 -> 359837 bytes
 docs/users_guide/glasgow_exts.xml                 |  211 +++++-
 73 files changed, 3091 insertions(+), 1060 deletions(-)

comment:44 Changed 4 years ago by goldfire

Resolution: fixed
Status: newclosed

A long-standing bug finally put to rest.

comment:45 Changed 4 years ago by goldfire

Test Case: deriving/should_fail/T1496
Note: See TracTickets for help on using tickets.