[GHC] #8678: Derivin `Functor` complains about existential type
#8678: Derivin `Functor` complains about existential type ------------------------------------+------------------------------------- Reporter: heisenbug | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.7 Keywords: | Operating System: Unknown/Multiple Architecture: Unknown/Multiple | Type of failure: None/Unknown Difficulty: Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | ------------------------------------+------------------------------------- When deriving a functor with !DataKinds enabled {{{ {-# LANGUAGE DataKinds, DeriveFunctor, FlexibleInstances, GADTs, KindSignatures, StandaloneDeriving #-} data {- kind -} Nat = Z | S Nat data NonStandard :: Nat -> * -> * where Standard :: a -> NonStandard (S n) a Non :: NonStandard n a -> a -> NonStandard (S n) a deriving instance Show a => Show (NonStandard n a) deriving instance Functor (NonStandard n) }}} I get following error message {{{ NonStandard.hs:10:1: Can't make a derived instance of ‛Functor (NonStandard n)’: Constructor ‛Standard’ must not have existential arguments In the stand-alone deriving instance for ‛Functor (NonStandard n)’ }}} But the `Standard` constructor is not at all existential in the last type argument! -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8678> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#8678: Derivin `Functor` complains about existential type -------------------------------------+------------------------------------ Reporter: heisenbug | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by carter): where does the variable {{{n}}} get introduced in {{{Standard :: a -> NonStandard (S n) a}}} ? That seems existential -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8678#comment:1> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#8678: Derivin `Functor` complains about existential type -------------------------------------+------------------------------------ Reporter: heisenbug | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by heisenbug): Replying to [comment:1 carter]:
where does the variable {{{n}}} get introduced in {{{Standard :: a -> NonStandard (S n) a}}} ? That seems existential
No, it is a variable that appears in the type of the result, so it is not existential. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8678#comment:2> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#8678: Derivin `Functor` complains about existential type -------------------------------------+------------------------------------ Reporter: heisenbug | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by monoidal): My guess is that the type of `Standard` is rewritten to `m ~ S n => a -> NonStandard m a` (which is existential in `n`). Simpler test case: `data A t a where A :: A Int a deriving Functor`. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8678#comment:3> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#8678: Derivin `Functor` complains about existential type -------------------------------------+------------------------------------ Reporter: heisenbug | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by heisenbug): Replying to [comment:3 monoidal]:
My guess is that the type of `Standard` is rewritten to `m ~ S n => a -> NonStandard m a` (which is existential in `n`). Simpler test case: `data A t a where A :: A Int a deriving Functor`.
Yeah, this is Henry Ford polymorphism ("you can have your car in any color as long as it is black"). But still, `deriving Functor` should only concern itself with the last parameter, which is manifestly not existential. Also, the parameter referred to has kind `Nat`, and thus is irrelevant for endofunctors on `*`. Furthermore even your example establishes a //functional dependency// between `t ~ Int`, so it should not count as existential. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8678#comment:4> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#8678: Deriving `Functor` complains about existential type -------------------------------------+------------------------------------ Reporter: heisenbug | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8678#comment:5> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#8678: Deriving `Functor` complains about existential type -------------------------------------+------------------------------------ Reporter: heisenbug | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by Simon Peyton Jones <simonpj@…>): In [changeset:"cdac487bcd9928d77738f6e79ead7b9bb4bc00fd/ghc"]: {{{ #!CommitTicketReference repository="ghc" revision="cdac487bcd9928d77738f6e79ead7b9bb4bc00fd" Make -XDeriveFunctor more generous about non-last arguments (Trac #8678) When deriving Functor, Foldable, Traversable, we need only look at the way that the last type argument is treated. It's fine for there to be existentials etc, provided they don't affect the last type argument. See Note [Check that the type variable is truly universal] in TcDeriv. }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8678#comment:6> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#8678: Deriving `Functor` complains about existential type -------------------------------------------------+------------------------- Reporter: heisenbug | Owner: Type: bug | Status: Priority: normal | closed Component: Compiler | Milestone: Resolution: fixed | Version: 7.7 Operating System: Unknown/Multiple | Keywords: Type of failure: None/Unknown | Architecture: Test Case: | Unknown/Multiple deriving/should_compile/T8678 | Difficulty: Blocking: | Unknown | Blocked By: | Related Tickets: -------------------------------------------------+------------------------- Changes (by simonpj): * status: new => closed * testcase: => deriving/should_compile/T8678 * resolution: => fixed Comment: Good idea. I have liberalise what `deriving Functor` will do, so that it looks only at the way in which the last type parameter is used. This makes perfect sense. Let's not merge this; it's a new feature. Simon -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8678#comment:7> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
participants (1)
-
GHC