Backreasoning (with holes).

phadej commented 4 years ago

The example (by @kosmikus)

{-# LANGUAGE TemplateHaskell #-}

import Optics

data Person =
  MkPerson
    { _name :: String
    , _numbers :: (Int, Int)
    }

makeLenses ''Person

p :: Person
p = MkPerson "Frodo" (66, 88)

example :: Person
example = set (numbers % _) 33 p

causes far from optimal type errors:

src/LvO.hs:17:11: error:
    • Overlapping instances for Is (Join A_Lens l0) A_Setter
        arising from a use of ‘set’
      Matching instances:
        instance [overlappable] (TypeError ...) => Is k l
          -- Defined in ‘optics-core-0.2:Optics.Internal.Optic.Subtyping’
        instance Is k k
          -- Defined in ‘optics-core-0.2:Optics.Internal.Optic.Subtyping’
        instance Is A_Lens A_Setter
          -- Defined in ‘optics-core-0.2:Optics.Internal.Optic.Subtyping’
        ...plus four others
        (use -fprint-potential-instances to see them all)
      (The choice depends on the instantiation of ‘l0’
       To pick the first instance above, use IncoherentInstances
       when compiling the other instance declarations)
    • In the expression: set (numbers % _) 33 p
      In an equation for ‘example’: example = set (numbers % _) 33 p
   |
17 | example = set (numbers % _) 33 p
   |           ^^^^^^^^^^^^^^^^^^^^^^

src/LvO.hs:17:16: error:
    • Overlapping instances for Is l0 (Join A_Lens l0)
        arising from a use of ‘%’
      Matching instances:
        instance [overlappable] (TypeError ...) => Is k l
          -- Defined in ‘optics-core-0.2:Optics.Internal.Optic.Subtyping’
        instance Is k k
          -- Defined in ‘optics-core-0.2:Optics.Internal.Optic.Subtyping’
        instance Is A_Getter A_Fold
          -- Defined in ‘optics-core-0.2:Optics.Internal.Optic.Subtyping’
        ...plus 35 others
        (use -fprint-potential-instances to see them all)
      (The choice depends on the instantiation of ‘l0’
       To pick the first instance above, use IncoherentInstances
       when compiling the other instance declarations)
    • In the first argument of ‘set’, namely ‘(numbers % _)’
      In the expression: set (numbers % _) 33 p
      In an equation for ‘example’: example = set (numbers % _) 33 p
   |
17 | example = set (numbers % _) 33 p
   |                ^^^^^^^^^^^

src/LvO.hs:17:26: error:
    • Found hole: _ :: Optic l0 js0 (Int, Int) (Int, Int) a0 Integer
      Where: ‘l0’ is an ambiguous type variable
             ‘js0’ is an ambiguous type variable
             ‘a0’ is an ambiguous type variable
    • In the second argument of ‘(%)’, namely ‘_’
      In the first argument of ‘set’, namely ‘(numbers % _)’
      In the expression: set (numbers % _) 33 p
    • Relevant bindings include
        example :: Person (bound at src/LvO.hs:17:1)
      Valid hole fits include
        ignored :: forall i s a b. IxTraversal i s s a b
          with ignored @i0 @(Int, Int) @a0 @Integer
          (imported from ‘Optics’ at src/LvO.hs:3:1-13
           (and originally defined in ‘Optics.IxTraversal’))
   |
17 | example = set (numbers % _) 33 p
   |                          ^

Yet technically we know that one needs something castable to Setter in this case. I.e. solving the equation:

k \/ ? = l

with

? = l

as it's least restricting option.

Can we make optics point that out?

adamgundry commented 4 years ago

Hmm, this seems tricky. The problem in the set (numbers % _) example is that there are two variables involved, and multiple possible choices of those variables. Assuming we give (%) some constraint Joinable, we have:

Is m A_Setter -- from call to set
Joinable A_Lens l m -- from call to %

These have multiple solutions, e.g. l ~ A_Setter, m ~ A_Setter but also l ~ An_Iso, m ~ A_Lens. We usually want to pick the former solution, because setters are notionally more general than isos, but as far as the type system is concerned there is no principal solution (and indeed, I might want to fill the hole with an iso, a setter or something else).

That said, we can possibly do a bit better in a case like numbers % _ :: Setter' Person Int . There we have Joinable A_Lens l A_Setter which really has principal solution l ~ A_Setter. At the moment we give this:

*Main Optics> :t numbers Optics.% _ :: Setter' Person Int

<interactive>:1:1: error:
    • Couldn't match type ‘Join A_Lens l0’ with ‘A_Setter’
        arising from a use of ‘Optics.%’
      The type variable ‘l0’ is ambiguous
    • In the expression: numbers Optics.% _ :: Setter' Person Int

<interactive>:1:18: error:
    • Found hole: _ :: Optic l0 '[] (Int, Int) (Int, Int) Int Int
      Where: ‘l0’ is an ambiguous type variable
    • In the second argument of ‘(Optics.%)’, namely ‘_’
      In the expression: numbers Optics.% _ :: Setter' Person Int
    • Valid hole fits include
        mapped :: forall (f :: * -> *) a b.
                  Functor f =>
                  Setter (f a) (f b) a b
          with mapped @((,) Int) @Int @Int
          (imported from ‘Optics’
           (and originally defined in ‘Optics.Setter’))

but we can get further if we define Joinable using incoherent instances to allow any two of its parameters to be supplied (see this gist for full details):

class (Is k m, Is l m, m ~ Join k l) => Joinable k l m

(%) :: forall k l m is js ks s t u v a b . (Joinable k l m, ks ~ Append is js)
     => Optic k is s t u v
     -> Optic l js u v a b
     -> Optic m ks s t a b
(%) = (Optics.%)

instance {-# INCOHERENT #-} l ~ A_Setter => Joinable A_Lens l A_Setter
instance {-# INCOHERENT #-} l ~ A_Setter => Joinable l A_Lens A_Setter
instance {-# INCOHERENT #-} l ~ A_Lens   => Joinable l A_Lens A_Lens
instance {-# INCOHERENT #-} l ~ A_Lens   => Joinable A_Lens l A_Lens
instance {-# INCOHERENT #-} l ~ A_Lens   => Joinable A_Lens A_Lens l

-- lots more instances here...

*Main Optics> :t numbers Main.% _ :: Setter' Person Int
<interactive>:1:16: error:
    • Found hole: _ :: Optic A_Setter '[] (Int, Int) (Int, Int) Int Int
    • In the second argument of ‘(Main.%)’, namely ‘_’
      In the expression: numbers Main.% _ :: Setter' Person Int
    • Valid hole fits include
        mapped :: forall (f :: * -> *) a b.
                  Functor f =>
                  Setter (f a) (f b) a b
          with mapped @((,) Int) @Int @Int
          (imported from ‘Optics’
           (and originally defined in ‘Optics.Setter’))

phadej commented 4 years ago

Yes, I oversimplified. We don't have k \/ x = l equality, but rather k \/ x <= l inequality. That can be simplified into x <= l, so it would be great if instead of the three error messages where the last is

src/LvO.hs:17:26: error:
    • Found hole: _ :: Optic l0 js0 (Int, Int) (Int, Int) a0 Integer
      Where: ‘l0’ is an ambiguous type variable
             ‘js0’ is an ambiguous type variable
             ‘a0’ is an ambiguous type variable

we would get

src/LvO.hs:17:26: error:
    • Found hole: _ :: Optic l0 js0 (Int, Int) (Int, Int) a0 Integer
      Where: ‘Is l0 A_Setter’
             ‘js0’ is an ambiguous type variable
             ‘a0’ is an ambiguous type variable

Note: I don't say l0 is a A_Setter by l0 ~ A_Setter, but using Is.

I'm tempted to try whether type-checker plugin could do this magic, even it's highly unpractical solution

phadej commented 4 years ago

A variation on above example is

{-# LANGUAGE TemplateHaskell #-}

import Optics

data Person =
  MkPerson
    { _name :: String
    , _numbers :: (Int, Int)
    }

makeLenses ''Person

p :: Person
p = MkPerson "Frodo" (66, 88)

numbers' :: Setter' Person (Int, Int)
numbers' = castOptic numbers

example2 :: Int
example2 = view (numbers' % _) p

where the errors are similar

Example.hs:20:12: error:
    • Overlapping instances for Is (Join A_Setter l0) 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 ‘l0’
       To pick the first instance above, use IncoherentInstances
       when compiling the other instance declarations)
    • In the expression: view (numbers' % _) p
      In an equation for ‘example2’: example2 = view (numbers' % _) p
   |
20 | example2 = view (numbers' % _) p
   |            ^^^^^^^^^^^^^^^^^^^^^

Example.hs:20:18: error:
    • Overlapping instances for Is l0 (Join A_Setter l0)
        arising from a use of ‘%’
      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_Getter A_Fold
          -- Defined in ‘Optics.Internal.Optic.Subtyping’
        ...plus 35 others
        (use -fprint-potential-instances to see them all)
      (The choice depends on the instantiation of ‘l0’
       To pick the first instance above, use IncoherentInstances
       when compiling the other instance declarations)
    • In the first argument of ‘view’, namely ‘(numbers' % _)’
      In the expression: view (numbers' % _) p
      In an equation for ‘example2’: example2 = view (numbers' % _) p
   |
20 | example2 = view (numbers' % _) p
   |                  ^^^^^^^^^^^^

Example.hs:20:29: error:
    • Found hole: _ :: Optic l0 js0 (Int, Int) (Int, Int) Int Int
      Where: ‘l0’ is an ambiguous type variable
             ‘js0’ is an ambiguous type variable
    • In the second argument of ‘(%)’, namely ‘_’
      In the first argument of ‘view’, namely ‘(numbers' % _)’
      In the expression: view (numbers' % _) p
    • Relevant bindings include
        example2 :: Int (bound at Example.hs:20:1)
   |
20 | example2 = view (numbers' % _) p
   |

But we know that there are no solution to Is (Join A_Setter l) A_Getter

arybczak commented 4 years ago

I think with the approach from #279 it would work better because then set would accept a Setter :thinking:

phadej commented 4 years ago

@arybczak in #279 we lose "forward reasoning", i.e. you cannot ask in GHCi what type foo % bar is. Same problem.

adamgundry commented 4 years ago

These kind of backwards reasoning problems feel annoyingly hard to solve with typeclasses. Given that the universe of optic kinds is finite and in principle closed, the machine ought to be able to do a better job of testing the various alternatives and complaining if there is a clear impossibility, but without backtracking it's hard to see how.

I've been playing around without a clear win yet. But I do have a couple of observations:

We could potentially replace the OVERLAPPABLE instance of Is k l with an instance for every k, l combination, yielding an error message if appropriate. That might yield a slightly better message in the case of an unsolved Is constraint blocked on a variable.
There are various options for how to encode the Joinable k l m constraint on (%). The current representation is (Is k m, Is l m, m ~ Join k l) but perhaps we can find a way to tweak this to avoid ending up with Is k (Join k l) constraints that are unnecessary (since if Join k l is defined then k must be below it by definition).

I'm tempted to try whether type-checker plugin could do this magic, even it's highly unpractical solution

I'm pretty sure a plugin could do better here. A plugin providing positive information would seem impractical, but I wonder if it would make sense to have a plugin that provides only negative information (i.e. spots constraints that cannot be solved and rewrites them into a form that yields a nicer error message)... clearly getting better errors without a plugin would be preferable though.

phadej commented 4 years ago

We could potentially replace the OVERLAPPABLE instance of Is k l with an instance for every k, l combination, yielding an error message if appropriate. That might yield a slightly better message in the case of an unsolved Is constraint blocked on a variable.

I tried that. It's "worse": the type variable is still ambiguous but there are now (always) 12 equations (of which 3 is shown and then "plus 9 others") - TypeError instances are still counted.

well-typed / optics

Backreasoning (with holes). #308