[GHC] #14661: Cannot derive (newtype I a b = I (F a -> F b) deriving newtype Category) for type family F
GHC
ghc-devs at haskell.org
Fri Jan 12 09:57:58 UTC 2018
#14661: Cannot derive (newtype I a b = I (F a -> F b) deriving newtype Category)
for type family F
-------------------------------------+-------------------------------------
Reporter: Iceland_jack | Owner: (none)
Type: feature request | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 8.4.1-alpha1
Resolution: | Keywords:
| DerivingStrategies, deriving,
| TypeFamilies
Operating System: Unknown/Multiple | Architecture:
| Unknown/Multiple
Type of failure: None/Unknown | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by simonpj):
Trac 14661
Hmm. What is `DerivingVia`? Is it implemented, documented?
I agree this is a feature request, going significantly beyond what GHC can
do right now.
However, the new feature looks tantalisingly close.
E.g. for `instance Category Ixed` we need to find
{{{
id :: forall a. Ixed a a
}}}
Expanding the type representation gives
{{{
id1 :: forall a. Interp a -> Interp a
}}}
We have in hand the `(->)` instance of `Category`:
{{{
id @(->) :: forall b. b -> b
}}}
and in fact we can readily instantiate `id @(->)@` to match the needed
type.
So, could we imagine this? Given
{{{
newtype N a b = MkN (R t1 t2 t3) deriving( Category )
}}}
we want to derive `instance ... => C N` given `instance ... => C R`.
Suppose we have a method in class `C`
{{{
class R (c :: * -> * -> *) where
foo :: forall p q. ...(c s1 s2)...
}}}
(NB: for now I will assume that `c` appears fully applied in `foo`'s
type.)
Then we will have available `foo1 :: forall p q. ...(R s1 s2)...`
and we want to get `foo2 :: forall p q. ...(N s1 s2)...`.
Well from the newtype declaration we have an axiom that equates the
representation
types of `(N a b)` and `(R t1 t2 t3)`:
{{{
ax :: forall a b. N a b ~R R t1 t2 t3
}}}
So, if we could find
{{{
foo3 :: forall p q. ...(R t1[s1/a,s2/q]
t2[s1/a,s2/q]
t3[s1/a,s2/q]) ...
}}}
we'd be home and dry, because then we can use `ax` to get from `foo3` to
`foo2`.
How can we get `foo3`? Well, it's possible that we can get it just by
instantiating
the type of `foo1`. In the case of `id` in `Category` we have
{{{
id1 :: forall a. (->) a a -- Available, given
id2 :: forall a. Ixed a a -- Wanted
id3 :: forall a. (->) (Interp a) (Interp a) -- Wanted
}}}
And indeed we can get `id3` from `id1` by instantiation.
This won't always work as Ryan points out, but sometimes.
And I suppose we could work that out.
It seems rather elaborate though!
--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14661#comment:9>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
More information about the ghc-tickets
mailing list