[GHC] #14440: Duplicate type family instances are permitted
#14440: Duplicate type family instances are permitted -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 (Type checker) | Keywords: TypeFamilies | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- 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: {{{#!hs {-# LANGUAGE TypeFamilies #-} module Lib where type family Foo b }}} {{{#!hs {-# LANGUAGE TypeFamilies #-} module A where import Lib type instance Foo Bool = Bool }}} {{{#!hs {-# LANGUAGE TypeFamilies #-} module B where import Lib type instance Foo Bool = Bool }}} {{{#!hs 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). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14440 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14440: Duplicate type family instances are permitted -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by AntC): Replying to [ticket:14440 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 [https://downloads.haskell.org/~ghc/8.2.1/docs/html/users_guide/glasgow_exts.... #compatibility-and-apartness-of-type-family-equations 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14440#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14440: Duplicate type family instances are permitted -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by AntC): Replying to [ticket:14440 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 [https://ghc.haskell.org/trac/ghc/ticket/10675#comment:15 '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 [https://github.com/ghc-proposals/ghc- proposals/pull/56 a way out]. Please upvote.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14440#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14440: Duplicate type family instances are permitted -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): See Section 3.6 of the [https://www.microsoft.com/en- us/research/publication/closed-type-families-with-overlapping-equations/ 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14440#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14440: Duplicate type family instances are permitted -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: invalid | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => closed * resolution: => invalid Comment: Ah, I wasn't aware that this had already been debated before. My apologies. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14440#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC