Multiparameter instance incorrectly considered partially overlapping

[fsoikin]

Description

See repro section for precise description of the symptoms. I'm not completely sure what the problem is, but it looks like the apartness check happens separately for each parameter of the instance, so that the instance may be considered partially overlapping if each parameter cannot be shown to be "apart" when considered in isolation, even if there is no possible substitution that would match all parameters together.

To Reproduce

newtype N a = N a

class C a b
instance C (N a) (N a)
else instance C a (N a)

x :: forall a. C a (N a) => Unit
x = unit

y :: Unit
y = x

The last line yields an error:

No type class instance was found for C t0 (N t0)
The following instance partially overlaps ...
    instance C (N a) (N a)

How can C (N a) (N a) possibly overlap C t0 (N t0)? That would require t0 ~ N t0.

Expected behavior

The second instance should be chosen, allowing the program to compile.

PureScript version

0.15.2

[rhendric]

That behavior is correct, as documented here: https://github.com/purescript/documentation/blob/master/language/Type-Classes.md#instance-chains (in response to @CarstenKoenig's comment, not the original post).

[rhendric]

Let's move this convo to the Discourse thread; pretty sure there's no issue here, and if there were it wouldn't be this issue (there are no multiparameter classes involved).

[rhendric]

Back on topic: @fsoikin, do you have a slightly more realistic repro of this issue? The minimal case you've provided would never work because a can't be determined in y = x. I can embellish this with Proxys and make it work but I want to make sure I'm capturing the use case you've abstracted this from.

[fsoikin]

Yes, of course.

But first, I'd like to note that the minimal example would, in fact, work, despite the fact that a cannot be determined. You can verify this by removing the first instance completely, leaving only instance C a (N a). With that change, the code compiles just fine. Since a is not actually used for anything, the compiler is apparently happy to leave it ambiguous.

---

But the original use case is, of course, rows. Isn't it always? :-)
The library in question is supposed to provide zero-runtime-cost coercion for partial records (i.e. records with some fields being undefined). The library itself is here, and the offending instance chain is here, but it's a bit involved, so I will reproduce it here in a somewhat simplified way.

The target API looks like this:

type ExpectedArgs = 
  { x :: Int   -- This field is required
  , y :: Opt String    -- This field is optional
  , z :: Opt Boolean    -- And so is this
  }

f :: ∀ args. CanBeCoerced args ExpectedArgs => args -> Int
f args' = args.x + ... (some implementation) ...
  where
    args = coerce args' :: ExpectedArgs

-- Use sites:
main = do 
  traceM $ f { x: 42 }  -- y and z omitted
  traceM $ f { x: 42, y: "foo" }  -- only z omitted
  traceM $ f { x: 42, y: "foo", z: false }  -- both present
  traceM $ f { x: 42, z: false }  -- only y omitted
  traceM $ f { x: 42, y: opt "foo", z: false }  -- y has type `Opt String` instead of `String`
  traceM $ f { x: 42, z: opt false }  -- z has type `Opt Boolean` instead of `Boolean`

The Opt wrapper is defined as a foreign type, intended to directly model JavaScript values that could be undefined, and accompanied by some functions to work with it. But for the present purposes we can assume it's just a newtype:

newtype Opt a = Opt a

opt :: ∀ a. a -> Opt a
opt = Opt

The interesting part is the CanBeCoerced class. For the above to work, it should walk the two records, compare labels and types as it goes, but skip fields marked with Opt if they're not present in the other record. The definition is quite straightforward:

class CanBeCoerced a b
instance CanBeCoerced a b => CanBeCoerced (Opt a) (Opt b)
else instance CanBeCoerced a b => CanBeCoerced a (Opt b)
else instance (RowToList a al, RowToList b bl, CanBeCoercedRL al bl) => CanBeCoerced (Record a) (Record b)
else instance TypeEquals a b => CanBeCoerced a b

class CanBeCoercedRL (a :: RowList Type) (b :: RowList Type)
instance CanBeCoercedRL Nil Nil
else instance (CanBeCoerced x y, CanBeCoercedRL a b) => CanBeCoercedRL (Cons label x a) (Cons label y b)
else instance CanBeCoercedRL a b => CanBeCoercedRL a (Cons label (Opt y) b)

coerce :: ∀ a b. CanBeCoerced a b => a -> b
coerce = unsafeCoerce

With this, all of the above examples work.
The fun starts when we make things generic. Consider this more sophisticated case:

type ExpectedArgsG a = { x :: a, y :: Opt a }

g :: ∀ args a. CanBeCoerced args (ExpectedArgsG a) => Show a => args -> Int
g args' = ...
  where
    args = coerce args' :: ExpectedArgsG a

With this, I would expect to be able to:

main = do
  traceM $ g { x: 42 }
  traceM $ g { x: 42, y: 5 }

Alas, this doesn't work (after the new apartness check in 0.15), because the choice of instance depends on the choice of a: the instance CanBeCoerced a (Opt b) may or may not match, so the compiler complains that it "partially overlaps". Ok, fair enough.

To work around that issue (and here's a pull request for it), I introduce a way to explicitly mark required fields, which is done with a new type Req:

newtype Req a = Req a

type ExpectedArgsG a = { x :: Req a, y :: Opt a }

This allows me to match on Req explicitly first thing in the chain and avoid the overlap:

class CanBeCoerced a b
instance TypeEquals a b => CanBeCoerced a (Req b)
else instance CanBeCoerced a b => CanBeCoerced (Opt a) (Opt b)
else instance CanBeCoerced a b => CanBeCoerced a (Opt b)
else instance (RowToList a al, RowToList b bl, CanBeCoercedRL al bl) => CanBeCoerced (Record a) (Record b)
else instance TypeEquals a b => CanBeCoerced a b

Now the above example with g works.
But we're not done yet! Let's introduce another level of parametricity:

h :: ∀ a. Show a => a -> Int
h a = g { x: a, y: a }

Now this doesn't compile, finally producing the error at the root of this issue:

No type class instance was found for

    Main.CanBeCoerced a2
                      (Opt a2)

  The following instance partially overlaps the above constraint, which means the rest of its instance chain will not be considered:

    instance in module Main with type forall a b. CanBeCoerced (Opt a) (Opt b)


while solving type class constraint

  Main.CanBeCoercedRL (Cons @Type "y" a2 (Nil @Type))
                      (Cons @Type "y" (Opt t1) (Nil @Type))

---

For convenience, here's the full program, from beginning to end. It fails to compile with the above error, but commenting h out allows it to compile.

module Main where

import Prelude

import Data.Maybe (Maybe(..), fromMaybe)
import Data.Newtype (class Newtype, unwrap)
import Data.String (length)
import Debug (traceM)
import Effect (Effect)
import Prim.RowList (class RowToList, Cons, Nil, RowList)
import Type.Equality (class TypeEquals)
import Unsafe.Coerce (unsafeCoerce)

newtype Opt a = Opt a

newtype Req a = Req a
derive instance Newtype (Req a) _

toMaybe :: ∀ a. Opt a -> Maybe a
toMaybe (Opt a) = Just a -- bogus implementation, just a placeholder!

opt :: ∀ a. a -> Opt a
opt = Opt

class CanBeCoerced a b
instance TypeEquals a b => CanBeCoerced a (Req b)
else instance CanBeCoerced a b => CanBeCoerced (Opt a) (Opt b)
else instance CanBeCoerced a b => CanBeCoerced a (Opt b)
else instance (RowToList a al, RowToList b bl, CanBeCoercedRL al bl) => CanBeCoerced (Record a) (Record b)
else instance TypeEquals a b => CanBeCoerced a b

class CanBeCoercedRL (a :: RowList Type) (b :: RowList Type)
instance CanBeCoercedRL Nil Nil
else instance (CanBeCoerced x y, CanBeCoercedRL a b) => CanBeCoercedRL (Cons label x a) (Cons label y b)
else instance CanBeCoercedRL a b => CanBeCoercedRL a (Cons label (Opt y) b)

coerce :: ∀ a b. CanBeCoerced a b => a -> b
coerce = unsafeCoerce

type ExpectedArgsG a = { x :: Req a, y :: Opt a }

g :: ∀ args a. CanBeCoerced args (ExpectedArgsG a) => Show a => args -> Int
g args' =
  (args.x # unwrap # show # length) + (args.y # toMaybe <#> show <#> length # fromMaybe 0)
  -- ^ Just some implementation to make sure the type variable isn't left ambiguous
  where
    args = coerce args' :: ExpectedArgsG a

h :: ∀ a. Show a => a -> Int
h a = g { x: a, y: a }

main :: Effect Unit
main = do
  traceM $ g { x: 42 }
  traceM $ g { x: 42, y: 5 }
  traceM $ g { x: 42, y: opt 5 }

[rhendric]

But first, I'd like to note that the minimal example would, in fact, work

Thanks, yes indeed, I stand corrected.

That example is helpful; thank you! I'm not sure that code ought to compile but I could be wrong about this again. In this case, you (eventually) want to solve the constraint CanBeCoerced a0 (Opt a0), and this is a potential match for CanBeCoerced (Opt a) (Opt b) if Opt a ~ a0 and b ~ a0, which I think doesn't require any infinite types or anything else the compile would know is impossible at this step. Do you agree?

[fsoikin]

Oh yes, you're absolutely right: it's not the same error. In my initial post (N a) (N a) is being matched with a (N a), but in my extended example a (Opt a) is being matched (Opt a) (Opt b). There is a b, not just a.

This is why a distilled example is better: less stuff to get confused about :-)

But yes, I remember now: this was exactly my train of thought, and to work around that, I added another a (Opt a) instance, so the whole chain looks like this:

class CanBeCoerced a b
instance CanBeCoerced a (Opt a)
else instance TypeEquals a b => CanBeCoerced a (Req b)
else instance CanBeCoerced a b => CanBeCoerced (Opt a) (Opt b)
else instance CanBeCoerced a b => CanBeCoerced a (Opt b)
else instance (RowToList a al, RowToList b bl, CanBeCoercedRL al bl) => CanBeCoerced (Record a) (Record b)
else instance TypeEquals a b => CanBeCoerced a b

With that, h, as defined above, compiles fine.
But then, my actual real-world example was also a bit different:

h :: ∀ a. Show a => a -> Int
h a = g { x: a, y: opt a }
--                 ^^^ this part is new

Now that finally yields the original error:

 No type class instance was found for

    Main.CanBeCoerced a2
                      a2

  The following instance partially overlaps the above constraint, which means the rest of its instance chain will not be considered:

    instance in module Main with type forall a. CanBeCoerced a (Opt a) (line 26, column 1 - line 26, column 32)


while solving type class constraint

  Main.CanBeCoerced (Opt a2)
                    (Opt a2)

Claiming that a2 a2 partially overlaps with a (Opt a), which I think can only be when a2 ~ a and a2 ~ Opt a implying a ~ Opt a.

However, while trying to recreate it again, I accidentally stumbled on further solution: if I add another instance for CanBeCoerced (Opt a) (Opt a), the last problem also goes away. So my concrete problem seems to be solved now (until next time ;-)

Nevertheless, I think this could be considered a compiler bug: it's still claiming an impossible partial overlap.

[rhendric]

Yeah, the original example (and this latest one) is certainly buggy behavior. I was only asking for clarification because I had a somewhat narrow fix in mind and wanted to know if the problem was broader than I was thinking. It still might be, but it looks like the narrow thing would do the right thing for this library at least.

[fsoikin]

Oh, that's great to hear! To be honest, I didn't really expect a fix :-)

[JordanMartinez]

The full code that triggers the error is:

module Main where

import Prelude

import Data.Maybe (Maybe(..), fromMaybe)
import Data.Newtype (class Newtype, unwrap)
import Data.String (length)
import Debug (traceM)
import Effect (Effect)
import Prim.RowList (class RowToList, Cons, Nil, RowList)
import Type.Equality (class TypeEquals)
import Unsafe.Coerce (unsafeCoerce)

newtype Opt a = Opt a

newtype Req a = Req a
derive instance Newtype (Req a) _

toMaybe :: ∀ a. Opt a -> Maybe a
toMaybe (Opt a) = Just a -- bogus implementation, just a placeholder!

opt :: ∀ a. a -> Opt a
opt = Opt

class CanBeCoerced a b
instance CanBeCoerced a (Opt a)
else instance TypeEquals a b => CanBeCoerced a (Req b)
else instance CanBeCoerced a b => CanBeCoerced (Opt a) (Opt b)
else instance CanBeCoerced a b => CanBeCoerced a (Opt b)
else instance (RowToList a al, RowToList b bl, CanBeCoercedRL al bl) => CanBeCoerced (Record a) (Record b)
else instance TypeEquals a b => CanBeCoerced a b

class CanBeCoercedRL (a :: RowList Type) (b :: RowList Type)
instance CanBeCoercedRL Nil Nil
else instance (CanBeCoerced x y, CanBeCoercedRL a b) => CanBeCoercedRL (Cons label x a) (Cons label y b)
else instance CanBeCoercedRL a b => CanBeCoercedRL a (Cons label (Opt y) b)

coerce :: ∀ a b. CanBeCoerced a b => a -> b
coerce = unsafeCoerce

type ExpectedArgsG a = { x :: Req a, y :: Opt a }

g :: ∀ args a. CanBeCoerced args (ExpectedArgsG a) => Show a => args -> Int
g args' =
  (args.x # unwrap # show # length) + (args.y # toMaybe <#> show <#> length # fromMaybe 0)
  -- ^ Just some implementation to make sure the type variable isn't left ambiguous
  where
    args = coerce args' :: ExpectedArgsG a

h :: ∀ a. Show a => a -> Int
h a = g { x: a, y: opt a }
--                 ^^^ this part is new

main :: Effect Unit
main = do
  traceM $ g { x: 42 }
  traceM $ g { x: 42, y: 5 }
  traceM $ g { x: 42, y: opt 5 }

[MonoidMusician]

Might be a duplicate of #4135? It isn't helped by the fundep issues fixed by #4195.

[rhendric]

I don't see any fundeps in these examples. #4135 might interact with #4195 but I'd be surprised if this does, unless the old covering set algorithm was so egregious that it doesn't return only the entire set of parameters when there are no fundeps. (... Is it that egregious?)

[MonoidMusician]

No I'm agreeing that I don't think #4135 was about fundeps, so it's probably about this issue instead. (Parameters only considered locally in terms of the overlaps check, instead of globally in relation to the other parameters.)

[MonoidMusician]

Maybe we should say that the other issue is a duplicate of this one, if we invent time-travel :)

[rhendric]

Ohhh I see, yeah, could be!

[drathier]

I tried to upgrade a project to 0.15.4 from 0.14.5 and I think I hit this case too:

h :: ∀ a. Show a => a -> Int
h a = g { x: a, y: a }

We're using this to convert types to similar types which are FFI-stable and deterministic, like flattening Data.Map into a sorted Array of Tuples. For that, we have a Storable a b => constraint instead of the Show a constraint above. Storable a b also has a functional dependency a -> b, and we're combining this with HMap to walk over record fields to convert records.

StatusHistory { what :: a0
              , when :: DateTime
              }
              { what :: b1
              , when :: DateTimeStorable
              }

Here what is polymorphic and uses Storable a b to convert the entire thing to a different format:

data StatusHistory r = StatusHistory (NonEmptyArray { when :: DateTime, what :: r })

data StatusHistoryStorable r
  = StatusHistoryStorableV1 (Array { when :: DateTimeStorable, what :: r })
  | StatusHistoryStorableV2 (NonEmptyArrayStorable { when :: DateTimeStorable, what :: r })

instance Storable a b => Storable (StatusHistory a) (StatusHistoryStorable b) where
  toStorable v =
    case v of
      StatusHistory h -> StatusHistoryStorableV2 (toStable h)
  fromStorable v = 

[drathier]

Turns out we didn't need the problematic type class instance. It's still worth reporting and fixing though, since it compiled fine in 0.14 but not in 0.15.

Let me know if you want me to minimize it further, it became pretty clear to me that the issue was at line 80-ish when I wrote the code below so I didn't reduce it further.

code is here

module Main where

-- Scroll down to ISSUE, line 81

import Prelude

import Effect (Effect)


import Data.Array as Array
import Data.Array.NonEmpty (NonEmptyArray)
import Data.Array.NonEmpty as NEA
import Partial.Unsafe
import Data.DateTime
import Heterogeneous.Mapping (class HMap, class Mapping, hmap)
import Heterogeneous.Mapping (class HMap, class Mapping, hmap, mapping)
import Data.Array.NonEmpty as NEA


class
  Storable a b
  | a -> b where
  toSerializable :: a -> b
  fromSerializable :: b -> a


data IntStorable = IntStorable Int

data StatusHistory r = StatusHistory (NonEmptyArray { when :: Int, what :: r })

data StatusHistoryStorable r
  = StatusHistoryStorableV1 (Array { when :: IntStorable, what :: r })
  | StatusHistoryStorableV2 (NonEmptyArrayStorable { when :: IntStorable, what :: r })

instance Storable a b => Storable (StatusHistory a) (StatusHistoryStorable b) where
  toSerializable v =
    case v of
      StatusHistory h -> StatusHistoryStorableV2 (toSerializable h)
  fromSerializable v = unsafeCrashWith "asdf"


data NonEmptyArrayStorable a = NonEmptyArrayStorableV1 { head :: a, tail :: Array a }

instance Storable a b => Storable (NonEmptyArray a) (NonEmptyArrayStorable b) where
  toSerializable a =
    a
      # map toSerializable
      # NEA.uncons
      # NonEmptyArrayStorableV1
  fromSerializable (NonEmptyArrayStorableV1 { head, tail }) =
    NEA.appendArray (NEA.singleton (fromSerializable head)) (tail <#> fromSerializable)

instance Storable Int IntStorable where
  toSerializable i = IntStorable i
  fromSerializable (IntStorable i) = i

--------

instance
  Storable a b =>
  Mapping SerializeRecord a b where
  mapping SerializeRecord = toSerializable

instance
  Storable a b =>
  Mapping DeserializeRecord b a where
  mapping DeserializeRecord = fromSerializable

instance
  ( HMap (RecursiveMapping SerializeRecord) (Record a) (Record b)
  , HMap (RecursiveMapping DeserializeRecord) (Record b) (Record a)
  ) =>
  Storable (Record a) (Record b) where
  toSerializable x = hmap (RecursiveMapping SerializeRecord) x
  fromSerializable x = hmap (RecursiveMapping DeserializeRecord) x

-- Record helpers
data SerializeRecord = SerializeRecord

data DeserializeRecord = DeserializeRecord

-------


-- ISSUE is here, in practice we weren't actually using the `asd` case anymore, so commenting it out and leaving `qwe` worked. We had this to generate instances for nested records, but we don't have any nested records anymore. Anyway, it compiled in 0.14 and doesn't in 0.15.
newtype RecursiveMapping adt = RecursiveMapping adt

-- instance
--   asd ::
--   HMap (RecursiveMapping adt) (Record rin) (Record rout) =>
--   Mapping (RecursiveMapping adt) (Record rin) (Record rout) where
--   mapping f a = hmap f a
-- else 
instance qwe :: Mapping f a b => Mapping (RecursiveMapping f) a b where
  mapping (RecursiveMapping f) a = mapping f a


-------

main :: Effect Unit
main =
  pure unit

[rhendric]

@drather, I believe the compiler is behaving correctly on your example.

The error message produced by uncommenting the asd instance is:

  No type class instance was found for

    Heterogeneous.Mapping.Mapping (RecursiveMapping SerializeRecord)
                                  a3
                                  b5

  The following instance partially overlaps the above constraint, which means the rest of its instance chain will not be considered:

    Main.asd

Mapping is defined with a fundep such that the first two parameters determine the third. The constraint you're asking the compiler to solve contains a type variable in the second position. That type could be a Record, in which case asd is the correct instance. Or that type could be anything else, in which case qwe is the correct instance. The compiler can't know which is correct, so it fails.

This is new behavior as of 0.15.0; it's documented here, and #4149 is the PR that made the change.

[natefaubion]

I think there's another case of this in routing-duplex:
https://github.com/natefaubion/purescript-routing-duplex/blob/13702d4a73ac3eac1d8c09701fb06faca7073728/src/Routing/Duplex/Generic.purs#LL80C1-L86C60

Which can be observed here, resulting in

  No type class instance was found for

    Routing.Duplex.Generic.GRouteDuplexCtr a0
                                           (Argument a0)

  The following instance partially overlaps the above constraint, which means the rest of its instance chain will not be considered:

    Routing.Duplex.Generic.gRouteArgument

It considers this overlapping, but a0 can't potentially be Argument a0 in this case since it would be an infinite type.

I wonder if we could allow things like this to solve with an occurs check somehow?