headers
Mikhail Glushenkov | 8 Oct 2012 21:11
Picon
Gravatar

Safe Haskell and instance coherence

Hello,

It's a relatively well-known fact that GHC allows for multiple type
class instances for the same type to coexist in a single program. This
can be used, for example, to construct values of the type Data.Set.Set
that violate the data structure invariant. I was mildly surprised to
find out that this works even when Safe Haskell is turned on:

https://gist.github.com/3854294

Note that the warnings tell us that both instances are "[safe]" which
gives a false sense of security.

I couldn't find anything on the interplay between orphan instances and
Safe Haskell both in the Haskell'12 paper and online. Is this
something that the authors of Safe Haskell are aware of/are intending
to fix?

--

-- 
()  ascii ribbon campaign - against html e-mail
/\  www.asciiribbon.org   - against proprietary attachments
Permalink | Reply |
headers
Simon Marlow | 11 Oct 2012 11:24
Picon

Re: Safe Haskell and instance coherence

On 08/10/2012 20:11, Mikhail Glushenkov wrote:
> Hello,
>
> It's a relatively well-known fact that GHC allows for multiple type
> class instances for the same type to coexist in a single program. This
> can be used, for example, to construct values of the type Data.Set.Set
> that violate the data structure invariant. I was mildly surprised to
> find out that this works even when Safe Haskell is turned on:
>
> https://gist.github.com/3854294
>
> Note that the warnings tell us that both instances are "[safe]" which
> gives a false sense of security.
>
> I couldn't find anything on the interplay between orphan instances and
> Safe Haskell both in the Haskell'12 paper and online. Is this
> something that the authors of Safe Haskell are aware of/are intending
> to fix?

A fine point.  Arguably this violates the module abstraction guarantee, 
because you are able to discover something about the implementation of 
Set by violating its assumption that the Ord instance for a given type 
is always the same.

I don't know what we should do about this.  Disallowing orphan instances 
seems a bit heavy-handed. David, Simon, any thoughts?

(can someone forward this to David Mazieres? all the email addresses I 
have for him seem to have expired :-)
(Continue reading)

Permalink | Reply |
headers
Mikhail Glushenkov | 11 Oct 2012 15:30
Picon
Gravatar

Re: Safe Haskell and instance coherence

Hello Simon,

On Thu, Oct 11, 2012 at 11:24 AM, Simon Marlow <marlowsd <at> gmail.com> wrote:
> On 08/10/2012 20:11, Mikhail Glushenkov wrote:
>> I couldn't find anything on the interplay between orphan instances and
>> Safe Haskell both in the Haskell'12 paper and online. Is this
>> something that the authors of Safe Haskell are aware of/are intending
>> to fix?
>
> [...]
> I don't know what we should do about this.  Disallowing orphan instances
> seems a bit heavy-handed. David, Simon, any thoughts?

What about detecting duplicate instances at link time? We could put
information about all instances defined in a given module into the
.comment section of the corresponding .o file and then have a pre-link
step script extract this information from all .o files in the program
and check that there are no duplicate or conflicting instances.

--

-- 
()  ascii ribbon campaign - against html e-mail
/\  www.asciiribbon.org   - against proprietary attachments
Permalink | Reply |
headers
MigMit | 11 Oct 2012 15:54
Picon
Favicon

Re: Safe Haskell and instance coherence


On Oct 11, 2012, at 5:30 PM, Mikhail Glushenkov <the.dead.shall.rise <at> gmail.com> wrote:

> Hello Simon,
> 
> On Thu, Oct 11, 2012 at 11:24 AM, Simon Marlow <marlowsd <at> gmail.com> wrote:
>> On 08/10/2012 20:11, Mikhail Glushenkov wrote:
>>> I couldn't find anything on the interplay between orphan instances and
>>> Safe Haskell both in the Haskell'12 paper and online. Is this
>>> something that the authors of Safe Haskell are aware of/are intending
>>> to fix?
>> 
>> [...]
>> I don't know what we should do about this.  Disallowing orphan instances
>> seems a bit heavy-handed. David, Simon, any thoughts?
> 
> What about detecting duplicate instances at link time? We could put
> information about all instances defined in a given module into the
> .comment section of the corresponding .o file and then have a pre-link
> step script extract this information from all .o files in the program
> and check that there are no duplicate or conflicting instances.
> 

You have a bigger problem coming. Some extensions make multiple instances OK, even in Safe Haskell. For example:

{-# LANGUAGE FlexibleInstances, IncoherentInstances, Safe #-}
module Over where
data Nil = Nil
newtype Cons a = Cons a
class Number n where value :: n -> Integer
(Continue reading)

Permalink | Reply |
headers
Mikhail Glushenkov | 11 Oct 2012 16:23
Picon
Gravatar

Re: Safe Haskell and instance coherence

Hello,

On Thu, Oct 11, 2012 at 3:54 PM, MigMit <miguelimo38 <at> yandex.ru> wrote:
> You have a bigger problem coming. Some extensions make multiple instances OK, even in Safe Haskell. For example:
>
> {-# LANGUAGE FlexibleInstances, IncoherentInstances, Safe #-}
> [...]

Safe Haskell already disallows OverlappingInstances. If we add a
requirement that it must be unambiguous which instance declaration a
given type class constraint resolves to (taking into account instances
defined in all modules), I think it will be necessary to also disallow
IncoherentInstances.

--

-- 
()  ascii ribbon campaign - against html e-mail
/\  www.asciiribbon.org   - against proprietary attachments
Permalink | Reply |
headers
MigMit | 11 Oct 2012 16:33
Picon
Favicon

Re: Safe Haskell and instance coherence


On Oct 11, 2012, at 6:23 PM, Mikhail Glushenkov <the.dead.shall.rise <at> gmail.com> wrote:

> Hello,
> 
> On Thu, Oct 11, 2012 at 3:54 PM, MigMit <miguelimo38 <at> yandex.ru> wrote:
>> You have a bigger problem coming. Some extensions make multiple instances OK, even in Safe Haskell. For example:
>> 
>> {-# LANGUAGE FlexibleInstances, IncoherentInstances, Safe #-}
>> [...]
> 
> Safe Haskell already disallows OverlappingInstances.

It doesn't. Overlapping instances are allowed in safe modules, provided that they won't be used in other modules.
Permalink | Reply |
headers
Mikhail Glushenkov | 11 Oct 2012 16:42
Picon
Gravatar

Re: Safe Haskell and instance coherence

Hello,

On Thu, Oct 11, 2012 at 4:33 PM, MigMit <miguelimo38 <at> yandex.ru> wrote:
>
> On Oct 11, 2012, at 6:23 PM, Mikhail Glushenkov <the.dead.shall.rise <at> gmail.com> wrote:
>>
>> On Thu, Oct 11, 2012 at 3:54 PM, MigMit <miguelimo38 <at> yandex.ru> wrote:
>>> You have a bigger problem coming. Some extensions make multiple instances OK, even in Safe Haskell. For example:
>>>
>>> {-# LANGUAGE FlexibleInstances, IncoherentInstances, Safe #-}
>>> [...]
>>
>> Safe Haskell already disallows OverlappingInstances.
>
> It doesn't. Overlapping instances are allowed in safe modules, provided that they won't be used in other modules.

I stand corrected. Still, I think that something will have to be done
about IncoherentInstances if the aforementioned restriction will be
added.

--

-- 
()  ascii ribbon campaign - against html e-mail
/\  www.asciiribbon.org   - against proprietary attachments
Permalink | Reply |
headers
MigMit | 11 Oct 2012 17:59
Picon
Favicon

Re: Safe Haskell and instance coherence

I hate to admit it, but it seems to me now that one would need dependent types to guarantee Set's good behavior
(so that the dictionary for the Ord instance is contained within the Set type).

Отправлено с iPhone

Oct 11, 2012, в 18:42, Mikhail Glushenkov <the.dead.shall.rise <at> gmail.com> написал(а):

> Hello,
> 
> On Thu, Oct 11, 2012 at 4:33 PM, MigMit <miguelimo38 <at> yandex.ru> wrote:
>> 
>> On Oct 11, 2012, at 6:23 PM, Mikhail Glushenkov <the.dead.shall.rise <at> gmail.com> wrote:
>>> 
>>> On Thu, Oct 11, 2012 at 3:54 PM, MigMit <miguelimo38 <at> yandex.ru> wrote:
>>>> You have a bigger problem coming. Some extensions make multiple instances OK, even in Safe Haskell.
For example:
>>>> 
>>>> {-# LANGUAGE FlexibleInstances, IncoherentInstances, Safe #-}
>>>> [...]
>>> 
>>> Safe Haskell already disallows OverlappingInstances.
>> 
>> It doesn't. Overlapping instances are allowed in safe modules, provided that they won't be used in other modules.
> 
> I stand corrected. Still, I think that something will have to be done
> about IncoherentInstances if the aforementioned restriction will be
> added.
> 
> -- 
> ()  ascii ribbon campaign - against html e-mail
(Continue reading)

Permalink | Reply |

Gmane