[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
#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