Opened 2 years ago

Closed 2 years ago

#14440 closed bug (invalid)

Duplicate type family instances are permitted

Reported by: RyanGlScott Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 8.2.1
Keywords: TypeFamilies Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

This threw me for a loop recently. To my surprise, GHC is quite happy to allow duplicate type family instances, provided that their RHSes are the same:

{-# LANGUAGE TypeFamilies #-}
module Lib where

type family Foo b
{-# LANGUAGE TypeFamilies #-}
module A where

import Lib

type instance Foo Bool = Bool
{-# LANGUAGE TypeFamilies #-}
module B where

import Lib

type instance Foo Bool = Bool
module C where

import A
import B
import Lib

f :: Bool -> Foo Bool
f x = not x
$ /opt/ghc/8.2.1/bin/ghci C.hs
GHCi, version 8.2.1: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 4] Compiling Lib              ( Lib.hs, interpreted )
[2 of 4] Compiling B                ( B.hs, interpreted )
[3 of 4] Compiling A                ( A.hs, interpreted )
[4 of 4] Compiling C                ( C.hs, interpreted )
Ok, 4 modules loaded.
λ> :i Foo
type family Foo b :: *  -- Defined at Lib.hs:4:1
type instance Foo Bool = Bool   -- Defined at A.hs:6:15
type instance Foo Bool = Bool   -- Defined at B.hs:6:15

Is this intended? My intuition screams "no", since if we offer class instance coherence, it seems like one ought to offer type family instance coherence as well. At the same time, I can't think of any threat to type soundness imposed by this (although it's quite strange to see two duplicate type family instances in the output of :i with two completely different provenances).

Change History (4)

comment:1 in reply to:  description ; Changed 2 years ago by AntC

Replying to RyanGlScott:

Is this intended?

I'm not sure if intended for identical type family instances, but it's certainly to be expected for partially overlapping type family instances. See examples in User Guide.

My intuition screams "no", since if we offer class instance coherence, it seems like one ought to offer type family instance coherence as well.

The trouble with class instances is that we can't infer whether the rhs method expressions are equivalent in case of overlapping instance heads. Thus you can't have class instances with identical heads -- GHC doesn't try checking if the rhs's are identical. Contrariwise type family rhs's have a very simple structure, needing only alpha-renaming to determine if confluent.

At the same time, I can't think of any threat to type soundness imposed by this.

Quite. And that's the point in the papers that introduced type families circa 2008.

comment:2 in reply to:  1 Changed 2 years ago by AntC

Replying to RyanGlScott:

My intuition screams "no", since if we offer class instance coherence, ...

And the short answer to that is we don't offer and can't guarantee class instance coherence/consistency, if you're talking about FunDeps. See SPJ on bogus consistency check. (Sorry, but there's plenty of code abusing that consistency check, pioneered in GHC in the 2004 HList paper. Contrast Hugs never allowed such abuse. There is a way out. Please upvote.)

comment:3 Changed 2 years ago by simonpj

See Section 3.6 of the Closed type families paper. Having identical RHSs is a degenerate case of Definition 10.

But perhaps it's so degenerate that it should be reported with a warning; I'm not sure.

comment:4 Changed 2 years ago by RyanGlScott

Resolution: invalid
Status: newclosed

Ah, I wasn't aware that this had already been debated before. My apologies.

Note: See TracTickets for help on using tickets.