Label optics misbehavior when defined with phantom type

[SeungheonOh]

instance
  (k ~ A_Lens, a ~ Int, b ~ Int) =>
  LabelOptic "inside" k (Tagged tag a) (Tagged tag b) a b
  where
    labelOptic = lens (\(Tagged x) -> x) (\_ x -> Tagged x)

When trying to use following label optics definition, it won't work

this is the error when tag is explicit

-- $> view #inside (Tagged @"hello" 10)

    • Data constructor ‘Tagged’ doesn't have a field named ‘inside’
    • In the first argument of ‘view’, namely ‘#inside’
      In the expression: view #inside (Tagged 10)
      In an equation for ‘_test’: _test = view #inside (Tagged 10)
    |
394 | _test = view #inside (Tagged 10)
    |  

this is the error when tag is ambiguous

-- $> view #inside (Tagged 10)

error:
    • Overlapping instances for Is k0 A_Getter
        arising from a use of ‘view’
      Matching instances:
        instance [overlappable] (TypeError ...) => Is k l
          -- Defined in ‘Optics.Internal.Optic.Subtyping’
        instance Is k k -- Defined in ‘Optics.Internal.Optic.Subtyping’
        instance Is A_Lens A_Getter
          -- Defined in ‘Optics.Internal.Optic.Subtyping’
        ...plus two others
        (use -fprint-potential-instances to see them all)
      (The choice depends on the instantiation of ‘k0’
       To pick the first instance above, use IncoherentInstances
       when compiling the other instance declarations)
    • In the expression: view #inside (Tagged 10)
      In an equation for ‘_test’: _test = view #inside (Tagged 10)
    |
392 | _test = view #inside (Tagged 10)
    |         ^^^^

error:
    • Overlapping instances for LabelOptic
                                  "inside" k0 (Tagged s0 b0) (Tagged s0 b0) Int Int
        arising from the overloaded label ‘#inside’
      Matching instances:
        instance [overlappable] Optics.Label.GenericLabelOpticContext
                                  repDefined name k s t a b =>
                                LabelOptic name k s t a b
          -- Defined in ‘Optics.Label’
        ...plus one instance involving out-of-scope types
        (use -fprint-potential-instances to see them all)
      (The choice depends on the instantiation of ‘k0, k1, s0, b0’
       To pick the first instance above, use IncoherentInstances
       when compiling the other instance declarations)
    • In the first argument of ‘view’, namely ‘#inside’
      In the expression: view #inside (Tagged 10)
      In an equation for ‘_test’: _test = view #inside (Tagged 10)
    |
392 | _test = view #inside (Tagged 10)
    |   

It will work, however, when tag is explicit:

instance
  (k ~ A_Lens, a ~ Int, b ~ Int) =>
  LabelOptic "inside" k (Tagged "test" a) (Tagged "test" b) a b
  where
    labelOptic = lens (\(Tagged x) -> x) (\_ x -> Tagged x)

_test :: Int
_test = view #inside (Tagged @"test" 10)

-- >> 10

but this isn't really useful.

It seems like LabelOptic thinks generic implementation is more specific when dealing with these types with tags.

[phadej]

I cannot reproduce, loading a standalone file:

{-# LANGUAGE FunctionalDependencies, GADTs, DataKinds, UndecidableInstances #-}
{-# LANGUAGE FlexibleInstances, PolyKinds #-}
{-# LANGUAGE DeriveGeneric #-}

import Optics.Core
import Optics.Label
import GHC.Generics

newtype Tagged tag a = Tagged a
  deriving Generic

{-
instance
  (k ~ An_Iso, tag ~ tag') =>
  LabelOptic "inside" k (Tagged tag a) (Tagged tag' b) a b
  where
    labelOptic = iso (\(Tagged x) -> x) Tagged
-}

instance
  (k ~ A_Lens, a ~ Int, b ~ Int) =>
  LabelOptic "inside" k (Tagged tag a) (Tagged tag b) a b
  where
    labelOptic = lens (\(Tagged x) -> x) (\_ x -> Tagged x)

works in 8.6.5 and 9.4.1

% ghci-8.6.5 Tagged.hs
GHCi, version 8.6.5: http://www.haskell.org/ghc/  :? for help
Loaded package environment from /code/other-haskell/optics/.ghc.environment.x86_64-linux-8.6.5
Loaded GHCi configuration from /home/phadej/.ghci
[1 of 1] Compiling Main             ( Tagged.hs, interpreted )
Ok, one module loaded.
*Main> :set -XDataKinds -XOverloadedLabels -XTypeApplications 
*Main> view #inside (Tagged @"hello" 10)
10

I didn't even need to do tag ~ tag' thing, which is probably a good idea.

[adamgundry]

I'm also struggling to reproduce this. I wondered if {-# LANGUAGE IncoherentInstances #-} might be enabled for the module containing the instance, but the second error seems to suggest not.

[SeungheonOh]

The error was coming from missing PolyKinds extension. After adding it, it work as expected. Thank you.

Perhaps, it's a good idea to add PolyKinds to example provided in here?

[phadej]

Interesting. So the instance you defined in

instance
  (k ~ A_Lens, a ~ Int, b ~ Int) =>
  LabelOptic "inside" k (Tagged tag a) (Tagged tag b) a b
  where
    labelOptic = lens (\(Tagged x) -> x) (\_ x -> Tagged x)

as kind-default to tag :: *, and thus it wasn't used.

And if I modify my example to have

instance
  (k ~ A_Lens, a ~ Int, b ~ Int) =>
  LabelOptic "inside" k (Tagged (tag :: *) a) (Tagged tag b) a b
                                     -- ^ force mono-kind.
  where
    labelOptic = lens (\(Tagged x) -> x) (\_ x -> Tagged x)

I also get an error:

<interactive>:4:6: error:
    • Data constructor ‘Tagged’ doesn't have a field named ‘inside’
    • In the first argument of ‘view’, namely ‘#inside’
      In the expression: view #inside (Tagged @"hello" 10)
      In an equation for ‘it’: it = view #inside (Tagged @"hello" 10)

I'm not sure how we could word that in Optics.Label. That is not-uncommon but still rare occurrence of a more general problem of defining non-polykinded instance for otherwise polykinded type. Maybe @adamgundry has some ideas on that.

[adamgundry]

I see.

It would make sense to have a polykinded example in the Optics.Label docs, along with an explicit statement that PolyKinds must be enabled at the instance definition site (as well as at the datatype definition site). But given that this can only be a problem for orphan LabelOptic instances with PolyKinds off, it's a bit of an odd corner.

We could perhaps propose that GHC should warn about such instances, or more generally issue a warning when a polykinded type is silently defaulted. This seems rather similar to https://gitlab.haskell.org/ghc/ghc/-/issues/18059.