Opened 3 years ago

Last modified 4 weeks ago

#7102 new bug

Type family instance overlap accepted in ghci

Reported by: exbb2 Owned by:
Priority: normal Milestone:
Component: GHCi Version: 7.4.1
Keywords: Cc: exbb2@…, oerjan
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC accepts invalid program Test Case:
Blocked By: Blocking:
Related Tickets: Differential Revisions:

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 (9)

comment:1 Changed 3 years ago by igloo

  • difficulty set to Unknown
  • Resolution set to wontfix
  • Status changed from new to closed

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 3 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 3 years ago by simonpj@…

commit 232f1a2702684fe7f82a084213714adfa6162392

Author: Simon Peyton Jones <[email protected]>
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 4 weeks ago by oerjan

  • Cc oerjan added
  • Resolution wontfix deleted
  • Status changed from closed to new

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 4 weeks ago by oerjan (previous) (diff)

comment:5 Changed 4 weeks 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 4 weeks 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 4 weeks 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 4 weeks 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 4 weeks 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 4 weeks ago by simonpj (previous) (diff)
Note: See TracTickets for help on using tickets.