Opened 5 years ago

Closed 4 years ago

Last modified 4 years ago

#7148 closed bug (fixed)

generalized newtype and type families is unsound

Reported by: carter Owned by: simonpj
Priority: normal Milestone: 7.8.1
Component: Compiler (Type checker) Version: 7.6.1-rc1
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: deriving/should_fail/T7148
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

the code from http://joyoftypes.blogspot.com/2012/08/generalizednewtypederiving-is.html type checks in the release candidate

also see discussion here http://www.reddit.com/r/haskell/comments/y8kca/generalizednewtypederiving_is_very_very_unsafe/

(punch line: the generalized newtype deriving + type families or gadts allows users to write unsafeCoerce etc)

perhaps a simple near term solution is to have any module using generalized new type deriving be inferred to be unsafe by default?

Attachments (2)

badUnsafeGADT.hs (793 bytes) - added by carter 5 years ago.
the code for the bugs
badUnsafe.hs (745 bytes) - added by carter 5 years ago.
the code for the type family version of the bug

Download all attachments as: .zip

Change History (10)

Changed 5 years ago by carter

Attachment: badUnsafeGADT.hs added

the code for the bugs

Changed 5 years ago by carter

Attachment: badUnsafe.hs added

the code for the type family version of the bug

comment:1 Changed 5 years ago by carter

to clarify: tested code in ghci

comment:2 Changed 5 years ago by simonpj

difficulty: Unknown

See #1496.

comment:3 Changed 5 years ago by dterei

GND isn't allowed in Safe modules, so yes it already causes code using it to be inferred Unsafe.

comment:4 Changed 5 years ago by igloo

Component: CompilerCompiler (Type checker)
Milestone: 7.8.1
Owner: set to simonpj

comment:5 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:6 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:7 Changed 4 years ago by goldfire

Resolution: fixed
Status: newclosed

comment:8 Changed 4 years ago by goldfire

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