Opened 3 years ago

Closed 4 months ago

Last modified 3 months ago

#5498 closed bug (fixed)

Generalized newtype deriving allows creating of instances I can't create by hand

Reported by: dterei Owned by:
Priority: normal Milestone: 7.6.2
Component: Compiler Version: 7.3
Keywords: Cc: dimitris@…, sweirich@…
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Difficulty: Unknown
Test Case: deriving/should_fail/T5498 Blocked By: #1496
Blocking: Related Tickets:

Description (last modified by simonpj)

First here is a simple module that establishes a list where once created (with a min element) subsequent elements inserted should always be larger than the min:

-- | Here we expose a MinList API that only allows elements
-- to be inserted into a list if they are at least greater
-- than an initial element the list is created with.
module MinList (
        MinList,
        newMinList,
        insertMinList,
        printIntMinList
    ) where

data MinList a = MinList a [a]

newMinList :: Ord a => a -> MinList a
newMinList n = MinList n []

insertMinList :: Ord a => MinList a -> a -> MinList a
insertMinList s@(MinList m xs) n | n > m     = MinList m (n:xs)
                                 | otherwise = s

printIntMinList :: MinList Int -> IO ()
printIntMinList (MinList min xs) = putStrLn $ "MinList Int :: MinList " ++ show min ++ " " ++ show xs

Now I import this module and use generalized newtype deriving to create a function I couldn't create by hand:

{-# LANGUAGE GeneralizedNewtypeDeriving #-}
-- | We use newtype to create an isomorphic type to Int
-- with a reversed Ord dictionary. We now use the MinList
-- API of MinList to create a new MinList. Then we use newtype
-- deriving to convert the newtype MinList to an Int
-- MinList. This final result breaks the invariants of
-- MinList which shouldn't be possible with the exposed
-- API of MinList.
module Main where

import MinList

class IntIso t where
    intIso :: c t -> c Int

instance IntIso Int where
    intIso = id

newtype Down a = Down a deriving (Eq, IntIso)

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

fine :: MinList (Down Int)
fine = foldl (\x y -> insertMinList x $ Down y) (newMinList $ Down 0) [-1,-2,-3,-4,1,2,3,4]

bad :: MinList Int
bad = intIso fine

main = do
    printIntMinList bad

The problem here is the isoInt method where I can do:

isoInt :: MinList (Down Int) -> MinList Int

which I shouldn't be able to do since I don't have the constructors for MinList.

This is the reason I've currently disabled newtype deriving in Safe Haskell but potentially we can enable it if this bug is fixed.

Change History (11)

comment:1 Changed 3 years ago by simonpj

  • Cc dimitris@… sweirich@… added
  • Description modified (diff)

I believe that this bug is very closely related to #1496 (just look at the type of the class moethod in each case).

We have an as-yet-unimplemented solution to #1496, namely our POPL'11 paper Generative type abstraction and type level computation. I don't yet know if the same approach deals with the problem you identify in this ticket, but my nose tells me yes. I'm adding Stephanie and Dimitrios to the cc.

comment:2 Changed 3 years ago by simonmar

The fix is to reject the deriving clause with an error, right? Couldn't we fix that without any deep type checker changes, just with a syntactic restriction on what classes you can derive for a newtype?

comment:3 Changed 3 years ago by dterei

How much work would it be to implement the fix from the paper? I'm guessing its in a complex part of the compiler I have no knowledge of so am probably not really the right person for the job.

What about what Simon M proposes? I'm not sure if this would be enough though as you can also combine newtype deriving with GADTs or TypeFamilies? to cause segfaults which is something SafeHaskell tries to prevent.

comment:4 Changed 3 years ago by simonpj

I really don't know of a "simple syntactic restriction" that would do the job. And the "roles" paper requires thought about how to implement it. Definitely it must wait until the current stuff for kind inference is done.

Is this really ruining anyone's day?

Simon

comment:5 Changed 3 years ago by simonpj

  • Blocked By 1496 added

comment:6 Changed 2 years ago by igloo

  • Milestone set to 7.6.1

comment:7 Changed 20 months ago by igloo

  • Milestone changed from 7.6.1 to 7.6.2

comment:8 Changed 9 months ago by goldfire

  • Difficulty set to Unknown

See Roles for the concrete approach toward a solution to the seg-faulting problem. Roles won't fix the abstraction problem that is the main subject of this ticket, though.

comment:9 Changed 4 months ago by nomeata

  • Resolution set to fixed
  • Status changed from new to closed

This should not be possible any more: In the type intIso :: forall c. c t -> c Int, c’s type parameter is considered to be nominal, so coerce will not allow changing c (Down a) to c a any more. And GND is now based on Coercible...

comment:10 Changed 4 months ago by simonpj

  • Test Case set to deriving/should_fail/T5498

Indeed. The program is indeed rejected, although the error message is not fantastic. I've added it as a test.

I think you can enable GND in Safe Haskell.

Simon

comment:11 Changed 3 months ago by Simon Peyton Jones <simonpj@…>

Note: See TracTickets for help on using tickets.