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