How to avoid impredicative polymorphism and define lens of lens

185 views Asked by At

I am trying to generate lens for data type with a lens field.

data St st l = St {
  _st_s :: String,
  _st_lens :: Lens' st l
}

st_lens :: forall st l. Lens' (St st l) (Lens' st l)
st_lens = lens _st_lens (\s a -> s { _st_lens = a })

GHC 8.10.7 gives me an error:

Illegal polymorphic type:
    forall (f1 :: * -> *). Functor f1 => (l -> f1 l) -> st -> f1 st
  GHC doesn't yet support impredicative polymorphism
• In the expansion of type synonym ‘Lens’
2

There are 2 answers

1
Iceland_jack On BEST ANSWER
{-# Language ImpredicativeTypes #-}
{-# Language TypeApplications #-}
-- ..

st_lens :: forall st l. Lens' (St st l) (Lens' st l)
st_lens = lens @_ @(Lens' st l) _st_lens \s a -> s { _st_lens = a }
0
duplode On

With GHC 9.2 or above, you can turn on ImpredicativeTypes, as demonstrated by Iceland_jack's answer. If you can't switch GHC versions right now, one pre-9.2 alternative is storing your lens as an ALens, and then using either cloneLens or the adapted combinators to make use of it:

data St st l = St {
  _st_s :: String,
  _st_lens :: ALens' st l
}

st_lens :: forall st l. Lens' (St st l) (ALens' st l)
st_lens = lens _st_lens (\s a -> s { _st_lens = a })
ghci> ("foo", 15) ^# (St "bar" _1 ^. st_lens)
"foo"
ghci> ("foo", 15) ^. cloneLens (St "bar" _1 ^. st_lens)
"foo"