[GHC] #13398: Associated type family instance validity checking is too conservative
#13398: Associated type family instance validity checking is too conservative -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: high | Milestone: 8.2.1 Component: Compiler | Version: 8.1 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: #11450 Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- `mediabus-0.3.0.1` currently fails to build on GHC HEAD because of this regression. Here's a simplified program which exemplifies the issue: {{{#!hs {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} module Mediabus where data Nat data Rate data StaticTicks where (:/:) :: Nat -> Rate -> StaticTicks type ticks :/ rate = ticks ':/: rate class HasStaticDuration (s :: k) where type SetStaticDuration s (pt :: StaticTicks) :: k instance HasStaticDuration (t :/ r) where type SetStaticDuration (t :/ r) (t' :/ r') = t' :/ r' }}} This compiles fine on GHC 8.0.2, but on GHC HEAD, it gives an odd error: {{{ $ ~/Software/ghc2/inplace/bin/ghc-stage2 --interactive Bug.hs GHCi, version 8.1.20170307: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Mediabus ( Bug.hs, interpreted ) Bug.hs:19:8: error: • Polymorphic type indexes of associated type ‘SetStaticDuration’ (i.e. ones independent of the class type variables) must be distinct type variables Expected: SetStaticDuration (t :/ r) <tv> Actual: SetStaticDuration (t :/ r) (t' :/ r') where the `<tv>' arguments are type variables, distinct from each other and from the instance variables • In the type instance declaration for ‘SetStaticDuration’ In the instance declaration for ‘HasStaticDuration (t :/ r)’ | 19 | type SetStaticDuration (t :/ r) (t' :/ r') = t' :/ r' | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ }}} This error message comes from 8136a5cbfcd24647f897a2fae9fcbda0b1624035 (#11450). To fix it, you have to do a tiresome song and dance with auxiliary type families: {{{#!hs {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} module Mediabus where data Nat data Rate data StaticTicks where (:/:) :: Nat -> Rate -> StaticTicks type ticks :/ rate = ticks ':/: rate class HasStaticDuration (s :: k) where type SetStaticDuration s (pt :: StaticTicks) :: k instance HasStaticDuration (t :/ r) where type SetStaticDuration (t :/ r) pt = SSDTicks pt type family SSDTicks (pt :: StaticTicks) :: StaticTicks where SSDTicks (t' :/ r') = t' :/ r' }}} But after Simon's motivation for this change in https://ghc.haskell.org/trac/ghc/ticket/11450#comment:24, I'm still not convinced that the original program should be rejected. After all, this change was introduced so that associated type families with //multiple// would be rejected. But in the `SetStaticDuration` example above, there's only one equation, and it's a complete pattern match! So I'm failing to see why it should be rejected. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13398 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13398: Associated type family instance validity checking is too conservative -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: high | Milestone: 8.2.1 Component: Compiler | Version: 8.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #11450 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Upon further thought, I'm not even sure why this particular restriction was added in the first place. #11450 was about making the type variables used in a class instance head the same as the variables used in the same positions in the associated type family instances. This business about not allowing multiple associated type family instances feels completely orthogonal to that issue (indeed, I wasn't even aware of its existence until just now, as it seems to have been snuck in without a mention in the GHC 8.2 release notes). Moreover, this additional check is causing code in the wild to fail, and for reasons that I don't comprehend. Simon, what exactly is the problem with allowing code like what is shown in the original program? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13398#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13398: Associated type family instance validity checking is too conservative -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: high | Milestone: 8.2.1 Component: Compiler | Version: 8.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #11450 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Why did you not write (in the original) {{{ instance HasStaticDuration (t :/ r) where type SetStaticDuration (t :/ r) pt = pt }}} I suppose you'll say that since `StaticTicks` has only one data constructor, replacing `pt` by `(t' :/ r')` makes no difference. But what about {{{ type family F a :: StaticTicks }}} Now I suppose that `SetStaticDuration (t :/ r) (F Int)` will fail to reduce? Suppose `StaticTicks` had a second data constructor `Foo`. Would you still say that the instance should be accepted? I was just trying to enforce that the definition was complete, nothing deeper. There is nothing fundamentally wrong with a partial function I suppose. But really, what's wrong with just using a variable here? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13398#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13398: Associated type family instance validity checking is too conservative -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: high | Milestone: 8.2.1 Component: Compiler | Version: 8.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #11450 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Replying to [comment:2 simonpj]:
Why did you not write (in the original) ...
Because I didn't write this code. It's from Hackage.
But really, what's wrong with just using a variable here?
Because that trick will only work in very limited circumstances. To better illustrate the point I'm trying to make, imagine you instead had this code: {{{#!hs instance HasStaticDuration (t :/ r) where type SetStaticDuration (t :/r) (t' :/ r') = r' :/ t' }}} This is a perfectly legitimate associated type family instance, and moreover, it //requires// pattern-matching on the second argument to `SetStaticDuration` to define. Yet in GHC HEAD, you cannot do this—you necessarily must jump through hoops to accomplish the same thing. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13398#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13398: Associated type family instance validity checking is too conservative -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: high | Milestone: 8.2.1 Component: Compiler | Version: 8.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #11450 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj):
To better illustrate the point I'm trying to make, imagine you instead had this code:
Ah. Excellent point. An easy thing to do is simply to lift the check altogether. So the result would be * The args corresponding to the class parameters must be identical * The other args can be anything at all So we'd allow {{{ class C a where type F a b ... instance C Int where type F Int Bool = Char ... }}} That says nothing about what `F Int Char` might be; and you can only give instances for `F` inside a class `instance`, so you can't extend it later. We could get this simply by omitting the two `check_poly_arg` lines in `TcValidity.checkConsistntFamInst`: {{{ -- Check type args first (more comprehensible) ; checkTc (all check_arg type_shapes) pp_wrong_at_arg ; checkTc (check_poly_args type_shapes) pp_wrong_at_tyvars -- And now kind args ; checkTc (all check_arg kind_shapes) (pp_wrong_at_arg $$ ppSuggestExplicitKinds) ; checkTc (check_poly_args kind_shapes) (pp_wrong_at_tyvars $$ ppSuggestExplicitKinds) }}} Alternatively I suppose we could instead elaborate the check to allow single-constructor data types to be pattern matched as above. (Nestedly, I guess.) Alternatively, we could just make a refutable pattern into a warning. But watch out for `type F Int r r`, which demands equality. I don't know which is best. Whatever the outcome, would you like to push this through, Ryan? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13398#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13398: Associated type family instance validity checking is too conservative -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: high | Milestone: 8.2.1 Component: Compiler | Version: 8.1 Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #11450 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * keywords: => TypeFamilies -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13398#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13398: Associated type family instance validity checking is too conservative -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: patch Priority: high | Milestone: 8.2.1 Component: Compiler | Version: 8.1 Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #11450 | Differential Rev(s): Phab:D3302 Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => patch * differential: => Phab:D3302 Comment: I think your first proposal (simply omitting those two checks) would be ideal. I've implemented that in Phab:D3302. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13398#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13398: Associated type family instance validity checking is too conservative
-------------------------------------+-------------------------------------
Reporter: RyanGlScott | Owner: (none)
Type: bug | Status: patch
Priority: high | Milestone: 8.2.1
Component: Compiler | Version: 8.1
Resolution: | Keywords: TypeFamilies
Operating System: Unknown/Multiple | Architecture:
| Unknown/Multiple
Type of failure: None/Unknown | Test Case:
Blocked By: | Blocking:
Related Tickets: #11450 | Differential Rev(s): Phab:D3302
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Ryan Scott
#13398: Associated type family instance validity checking is too conservative -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: merge Priority: high | Milestone: 8.2.1 Component: Compiler | Version: 8.1 Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: indexed- | types/should_compile/T13398a, | indexed- | types/should_compile/T13398b Blocked By: | Blocking: Related Tickets: #11450 | Differential Rev(s): Phab:D3302 Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * testcase: => indexed-types/should_compile/T13398a, indexed- types/should_compile/T13398b * status: patch => merge -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13398#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13398: Associated type family instance validity checking is too conservative -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: high | Milestone: 8.2.1 Component: Compiler | Version: 8.1 Resolution: fixed | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: indexed- | types/should_compile/T13398a, | indexed- | types/should_compile/T13398b Blocked By: | Blocking: Related Tickets: #11450 | Differential Rev(s): Phab:D3302 Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * status: merge => closed * resolution: => fixed Comment: Merged to `ghc-8.2` as 82366c4c1501d57dd8490818ef6e0709aca8836f. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13398#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC