[GHC] #11416: GHC mistakenly believes datatype with type synonym in its type can't be eta-reduced
#11416: GHC mistakenly believes datatype with type synonym in its type can't be eta-reduced -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.1 (Type checker) | Keywords: TypeInType | Operating System: Unknown/Multiple Architecture: | Type of failure: GHC rejects Unknown/Multiple | valid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- I uncovered this when playing around with `-XTypeInType`: {{{#!hs {-# LANGUAGE DeriveFunctor, TypeInType #-} module CantEtaReduce1 where import Data.Kind type ConstantT a b = a newtype T (f :: * -> *) (a :: ConstantT * f) = T (f a) deriving Functor }}} This fails because it thinks that you can't reduce the last type variable of `T`, since it mentions another type variable (`f`): {{{ • Cannot eta-reduce to an instance of form instance (...) => Functor (T f) • In the newtype declaration for ‘T }}} But it ''should'' be able to, since `ConstantT * f` reduces to `*`, and the equivalent declaration `newtype T (f :: * -> *) (a :: *) = ...` eta- reduces just fine. I marked this as appearing in GHC 8.1 since you need `-XTypeInType` to have kind synonyms, but this can also happen in earlier GHC versions with data families: {{{#!hs {-# LANGUAGE DeriveFunctor, PolyKinds, TypeFamilies #-} module CantEtaReduce2 where type ConstantT a b = a data family T (f :: * -> *) (a :: *) newtype instance T f (ConstantT a f) = T (f a) deriving Functor }}} I believe the fix will be to apply `coreView` with precision to parts of the code which typecheck `deriving` statements so that these type synonyms are peeled off. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11416> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11416: GHC mistakenly believes datatype with type synonym in its type can't be eta-reduced -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: Type: bug | Status: patch Priority: normal | Milestone: Component: Compiler (Type | Version: 8.1 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D1772 Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => patch * differential: => Phab:D1772 -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11416#comment:1> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11416: GHC mistakenly believes datatype with type synonym in its type can't be eta-reduced -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: Type: bug | Status: patch Priority: normal | Milestone: Component: Compiler (Type | Version: 8.1 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D1772 Wiki Page: | -------------------------------------+------------------------------------- Comment (by Ben Gamari <ben@…>): In [changeset:"165ae440b6bbf577eabf0b6d422ed6ea3bf949b4/ghc" 165ae440/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="165ae440b6bbf577eabf0b6d422ed6ea3bf949b4" Expand type/kind synonyms in TyVars before deriving-related typechecking Before, it was possible to have a datatypes such as ``` type ConstantT a b = a newtype T (f :: * -> *) (a :: ConstantT * f) = T (f a) deriving Functor data family TFam (f :: * -> *) (a :: *) newtype instance TFam f (ConstantT a f) = TFam (f a) deriving Functor ``` fail to eta-reduce because either (1) a TyVar had a kind synonym that mentioned another TyVar, or (2) an instantiated type was itself a type synonym that mentioned another TyVar. A little bit of tweaking to `expandTypeSynonyms` and applying it before the eta-reduction check in the `deriving` machinery is sufficient to fix this. Fixes #11416. Test Plan: ./validate Reviewers: goldfire, simonpj, austin, bgamari Reviewed By: simonpj Subscribers: thomie Differential Revision: https://phabricator.haskell.org/D1772 GHC Trac Issues: #11416 }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11416#comment:2> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11416: GHC mistakenly believes datatype with type synonym in its type can't be eta-reduced -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: Type: bug | Status: merge Priority: normal | Milestone: 8.0.1 Component: Compiler (Type | Version: 8.0.1-rc1 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D1772 Wiki Page: | -------------------------------------+------------------------------------- Changes (by thomie): * status: patch => merge * version: 8.1 => 8.0.1-rc1 * milestone: => 8.0.1 -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11416#comment:3> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11416: GHC mistakenly believes datatype with type synonym in its type can't be eta-reduced -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: Type: bug | Status: closed Priority: normal | Milestone: 8.0.1 Component: Compiler (Type | Version: 8.0.1-rc1 checker) | Resolution: fixed | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D1772 Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * status: merge => closed * resolution: => fixed Comment: This was merged to `ghc-8.0` as 20f848b0e9020355340f3f0f2311d2f3d9aceb7c. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11416#comment:4> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11416: GHC mistakenly believes datatype with type synonym in its type can't be eta-reduced -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: Type: bug | Status: closed Priority: normal | Milestone: 8.0.1 Component: Compiler (Type | Version: 8.0.1-rc1 checker) | Resolution: fixed | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D1772 Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Hm, there's another tricky case that I hadn't previously considered: {{{#!hs type ConstT a b = a data family Fam a b data instance Fam (ConstT a b) b = Fam b deriving Functor }}} Currently, the eta-reduction check rejects this. Should it? On on hand, the `b` in `ConstT a b` will go away if you expand the `ConstT` type synonym, so one could argue this is no different from `data instance Fam a b = Fam b deriving Functor` (which is accepted). On the other hand, if you consider what the derived instance would look like: {{{#!hs instance Functor (Fam (ConstT a b)) where ... }}} This feels a bit off, because now the instance head is mentioning an eta- reduced type variable! But it does typecheck if you type it in manually... -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11416#comment:5> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#11416: GHC mistakenly believes datatype with type synonym in its type can't be eta-reduced -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: Type: bug | Status: closed Priority: normal | Milestone: 8.0.1 Component: Compiler (Type | Version: 8.0.1-rc1 checker) | Resolution: fixed | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D1772 Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Maybe. If you type it in manually you'll get a spuriously polymorphic instance, which will result in some uses of `Any`. I think the same will happen if you allow this data instance. Perhaps it's no more than using `exactTyCoVarsofType` in `eta_reduce` in `tcDataFamInstDecl`. You'd need to make sure you quantify over the tyvar anyway; but I think that will happen. I don't feel strongly. It would be good to document it. Crumbs if I had a pound for every hour I've spent on `GeneralisedNewtypeDeriving` I'd be a rich man. Thanks for digging into this -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11416#comment:6> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
participants (1)
-
GHC