haskellhaskell-lensimpredicativetypes

How to avoid impredicative polymorphism and define lens of lens


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’

Solution

  • {-# 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 }