Opened 5 years ago

Last modified 9 months ago

#7102 new bug

Type family instance overlap accepted in ghci

Reported by: exbb2 Owned by: rwbarton
Priority: normal Milestone:
Component: GHCi Version: 7.4.1
Keywords: TypeFamilies Cc: exbb2@…, oerjan
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC accepts invalid program Test Case: T7102a, T7102
Blocked By: Blocking:
Related Tickets: Differential Rev(s): Phab:D2994
Wiki Page:

Description

This code works if I paste it line by line in ghci, but not if i try to load or compile it.

{-# LANGUAGE TypeFamilies #-}

data Rec a b =  Rec {unRec :: Rec a b -> b}

class RecursiveFun f where type A a b :: *; recurse :: f (A a b) b -> b

instance RecursiveFun Rec where type A a b = a; recurse r = unRec r r

instance RecursiveFun (->) where type A a b = Rec a b; recurse f = f (Rec f)

Change History (14)

comment:1 Changed 5 years ago by igloo

difficulty: Unknown
Resolution: wontfix
Status: newclosed

I'm inclined to say that this is not a bug. In a similar way to how ghci lets you shadow variables:

Prelude> let f = 'a'
Prelude> let f = True
Prelude> f
True

it is letting you shadow type family instances:

Prelude> :set -XTypeFamilies
Prelude> type family F x :: *
Prelude> type instance F Int = Bool
Prelude> type instance F Int = Char
Prelude> :t undefined :: F Int
undefined :: F Int :: Char

I think that this makes sense: If you imagine that F is defined in some other package, and you are developing the type on the RHS, then if this were not possible then you'd have to restart ghci each time you alter the type.

comment:2 Changed 5 years ago by simonpj

It turns out that, as Ian says, this is by design. A new type instance declaration in GHCi replaces any earlier one with the same LHS.

But it was not documented, so I have added a note to the user manual to say so.

Simon

comment:3 Changed 5 years ago by simonpj@…

commit 232f1a2702684fe7f82a084213714adfa6162392

Author: Simon Peyton Jones <simonpj@microsoft.com>
Date:   Wed Oct 31 17:03:28 2012 +0000

    Add notes about type-family overlap in GHCi (see Trac #7102)

 docs/users_guide/ghci.xml         |    6 +++++-
 docs/users_guide/glasgow_exts.xml |    1 +
 2 files changed, 6 insertions(+), 1 deletions(-)

comment:4 Changed 2 years ago by oerjan

Cc: oerjan added
Resolution: wontfix
Status: closednew

I think this behavior should be reconsidered when Safe Haskell is enabled.

Prelude> :set -XSafe
Prelude> :seti -XSafe
Prelude> :set -XTypeFamilies
Prelude> type family T a b
Prelude> type instance T a b = a
Prelude> let uc :: a -> T a b; uc = id
Prelude> type instance T a b = b
Prelude> uc 'a' :: Int
97

(EDIT: Simplified)

Last edited 2 years ago by oerjan (previous) (diff)

comment:5 Changed 2 years ago by simonpj

That is indeed very very bad. Never mind Safe Haskell -- it's just unsound. You didn't get a seg fault, but you very well might have. (For class instances it wouldn't be unsound, just possibly a bit incoherent.)

I'm not sure what to do:

  1. Prohibit type instance declarations in GHCi that overlap/override earlier ones?
  1. Do (1) but also provide a way to purge the GHCi environment, so you can get back to a clean slate without restarting GHCi
  1. Try to be clever: purge only functions (or whatever) whose types mention T. But it's tricky: what about data types mentioning T, and functions whose types use those data types...

I incline to (2). Any other opinions?

comment:6 Changed 2 years ago by oerjan

I suspect the purging in (2) can already be achieved by just redeclaring the type family, after which new instances would refer to the new entity.

comment:7 Changed 2 years ago by oerjan

Since you said not to mind Safe Haskell, I also found a similar unsoundness that uses loading of modules instead. All the modules can be Safe, but GHCi itself cannot have the flag set.

{-# LANGUAGE Safe, TypeFamilies #-}

module T1 where

type family T a b
{-# LANGUAGE Safe, TypeFamilies #-}

module T2 where

import T1

type instance T a b = a

from :: a -> T a b
from = id
{-# LANGUAGE Safe, TypeFamilies #-}

module T3 where

import T1

type instance T a b = b

to :: T a b -> b
to = id

Now in GHCi:

Prelude> :l T2 T3
[1 of 3] Compiling T1               ( T1.hs, interpreted )
[2 of 3] Compiling T3               ( T3.hs, interpreted )
[3 of 3] Compiling T2               ( T2.hs, interpreted )
Ok, modules loaded: T2, T1, T3.
*T2> :m +T3
*T2 T3> let uc = to . from
*T2 T3> uc 'a' :: Int
97

comment:8 Changed 2 years ago by oerjan

Oh hm, of course, purging that easily only works when the type family isn't imported from a module.

comment:9 Changed 2 years ago by simonpj

Eek. Of course GHCi should do an eager instance-overlap check when loading modules, just as GHC does. That is a serious bug. Again, nothign to do with Safe Haskell; your example works just as well without {-# LANGUAGE Safe #-}.

Would anyone like to look at it? The code is all there, since it is used for dealing with imports in GHC.

I suspect the purging in (2) can already be achieved by just redeclaring the type family, after which new instances would refer to the new entity.

Ah yes, that is true. Clever. So this is what would happen

Prelude> type family T a b
Prelude> type instance T a b = a
Prelude> let uc :: a -> T a b; uc = id

Prelude> type instance T a b = b
ERROR: instance overlap

-- User thinks: darn!  Re-declare T
Prelude> type family T a b
-- This is a brand-new T, unrelated to the old one

Prelude> uc 'a' :: Int
<interactive>:6:1: error:
    Couldn't match type ‘Char’ with ‘Int’
    Expected type: Int
      Actual type: Ghci1.T Char b0

So, no need to add a new facility for purging. We just need to reject the overlap.

Simon

Last edited 2 years ago by simonpj (previous) (diff)

comment:10 Changed 21 months ago by thomie

Keywords: TypeFamilies added

comment:11 Changed 9 months ago by rwbarton

Owner: set to rwbarton

comment:12 Changed 9 months ago by rwbarton

Differential Rev(s): Phab:D2994
Test Case: T7102a, T7102

There are actually two issues in this ticket.

  • The original issue, that you can replace type family instances in ghci as in comment:1. There was special logic to allow this (copied from the case of class instances), so fixing it was just deleting code (that I was going to have to change anyways, for another issue). I added test T7102a for this one.
  • The issue in comment:7 is different, and doesn't rely on the two instances having the same LHS. It's apparently not that ghci is replacing one instance with the other one, but rather that it never checks that the two instances are consistent with each other. So we need an additional consistency check somewhere. I haven't fixed this yet, but I added a expect_broken test T7102 for it.

comment:13 Changed 9 months ago by oerjan

Perhaps the error message for the instance overlap could mention (if in GHCi) that you can get around it by redeclaring the type family.

comment:14 Changed 9 months ago by Ben Gamari <ben@…>

In 0abe7361/ghc:

Don't replace type family instances with the same LHS in GHCi (#7102)

This fixes the easy part of #7102 by removing the logic that lets the
user replace a type family instance with a new one with the same LHS.
As discussed on that ticket, this is unsound in general. Better to have
the user redefine the type family from scratch.

The example from comment:7 involving loading modules into ghci is not
fixed yet; it actually doesn't rely on the instances having the same LHS.
This commit adds an expect_broken test for that example as well.

Test Plan: T7102a for the fix; T7102 is the test not fixed yet

Reviewers: dfeuer, austin, bgamari, goldfire

Reviewed By: dfeuer

Subscribers: dfeuer, thomie

Differential Revision: https://phabricator.haskell.org/D2994
Note: See TracTickets for help on using tickets.