Why doesn't makeLenses derive a lens for some quantified constructors?

user_2659595 0
Viewed 75

I'm trying to make lenses for a slightly complex GADT, and finding it doesn't want to generate one for one of my constructors. The code looks like this:

{-# LANGUAGE GADTs, RankNTypes, TemplateHaskell, KindSignatures, DataKinds #-}

import Control.Lens
import GHC.TypeNats

data Variant (m :: Nat) where
  VariantA :: Variant 42

data Stuff where
  Foo :: { _foo :: Int } -> Stuff
  Bar :: forall t. { _bar :: String } -> Stuff
  Baz :: forall m. { _baz :: Variant m } -> Stuff

$(makeLenses ''Stuff)

I find that this generates lenses foo and bar, but not baz. It seems to be something to do with the constraint on baz and the kind signature Variant m. Why can't I get a lens for baz?

I saw that some support for existentially quantified record constructors was added at the end of https://github.com/ekmett/lens/issues/409, but wondering if this is a further lens issue.

haskell-lens gadt haskell
1 Answers

The problem isn't with makeLenses. The problem is that you really can't write a Traversal, or even a Setter, for _baz. Let's see what happens when you try to write a Traversal:

baz :: Traversal' Stuff (Variant m)
baz f (Baz v) = _
baz _f s = pure s

GHC says:

LensGADT.hs:19:17: error:
    • Found hole: _ :: f Stuff
      Where: ‘f’ is a rigid type variable bound by
               the type signature for:
                 baz :: forall (m :: Nat). Traversal' Stuff (Variant m)
               at LensGADT.hs:18:1-35
    • In the expression: _
      In an equation for ‘baz’: baz f (Baz v) = _
    • Relevant bindings include
        v :: Variant m1 (bound at LensGADT.hs:19:12)
        f :: Variant m -> f (Variant m) (bound at LensGADT.hs:19:5)
        baz :: (Variant m -> f (Variant m)) -> Stuff -> f Stuff
          (bound at LensGADT.hs:19:1)
      Constraints include Applicative f (from LensGADT.hs:18:1-35)
   |
19 | baz f (Baz v) = _
   |                 ^

You see the problem? We're given a function of type Variant m -> f (Variant m) for some m, and we have a value of type Variant m1, for some (possibly different) m1. We can't possibly apply the function! Exactly the same problem shows up if you try to write a setter.

The best you could do is this:

baz1 :: Applicative f => (forall m. Variant m -> f (Variant m)) -> Stuff -> f Stuff
baz1 f (Baz v) = Baz <$> f v
baz1 _f s = pure s

or this (same code, slightly different type):

baz2 :: Applicative f => (forall m. Variant m -> f (Variant n)) -> Stuff -> f Stuff
baz2 f (Baz v) = Baz <$> f v
baz2 _f s = pure s

These are very much like traversals, but they're certainly not Traversals in the lens sense. Moreover, neither of them is strictly more general than the other, and a more flexible version that subsumes both will look significantly less like a Traversal. So it doesn't seem that reasonable for makeLenses to even try.

user_14776670
Related