Wingman produces ill-typed term

[isovector]

Another weird one from @masaeedu:

{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE DataKinds #-}

import Prelude hiding (id, (.))
import Control.Category
import Data.List.NonEmpty

data Index f as
  where
  Head :: f a -> Index f (a ':| as)
  Next :: Index f (a ':| as) -> Index f (x ':| a ': as)

newtype Flip p a b = Flip { runFlip :: p b a }

data Smoosh p as bs
  where
  Terminal :: Smoosh p as '[]
  Projection :: Index (Flip p b) (a ':| as) -> Smoosh p (a ': as) bs -> Smoosh p (a ': as) (b ': bs)

heteroCompose
  :: Category p
  => Index (Flip p c) (b ':| bs)
  -> Smoosh p (a ': as) (b ': bs)
  -> Index (Flip p c) (a ':| as)
heteroCompose = _

Wingman produces this:

heteroCompose (Head fl) _ = Head fl
heteroCompose (Next in') _ = Next in'

which doesn't type-check. The real solution should be

heteroCompose = \case
  Head (Flip pbc) -> \(Projection (Head (Flip pab)) _) -> Head $ Flip $ pbc . pab
  Next v          -> \(Projection _                 r) -> heteroCompose v r

[isovector]

For some reason it thinks it can turn f a into f b in the Head case, where f ~ Flip p c. But this shouldn't possibly unify, given that everything involved is a skolem:

!!!skolems: fromList [a,p,c,b,bs,a,as]

[isovector]

This is probably the same bug as #2171

[isovector]

A simpler repro:

data Index xs where
  Head :: x -> Index (x ':| xs)

heteroCompose
  :: Index b
  -> Index a
heteroCompose = _

[isovector]

I think what's happening here is when we split Index, we learn exists x xs. b ~ (x ':| xs). But x and xs should be rigid skolems, and I bet they're being instantiated as unification variables.

[isovector]

That doesn't appear to be the case:

!!!adding skolems: [x,xs]
!!!adding theta: [b ~ (x ':| xs)]

So maybe the problem is in assumption, thinking it can unify skolem a with skolem x?

[isovector]

Curiously, the assumption succeeds:

!!!successfully unified: (x,x)
!!!with skolems: fromList [x,xs,a,b]

So the goal when constructing Head is x! But this is odd. Because what ARE we trying to produce? It's not entirely clear. We know that exists y ys. a ~ (y ':| ys). Therefore, we want to be producing a y, but it's unclear why that existential y can't be the existential x.

[isovector]

The type error from ghc is this:

• Could not deduce: b ~ (x ':| xs0)
  from the context: a ~ (x ':| xs)
    bound by a pattern with constructor:
               Head :: forall x (xs :: [*]). x -> Index (x ':| xs),
             in an equation for ‘heteroCompose’
    at /home/sandy/prj/tesths/src/Lib.hs:14:16-21
  ‘b’ is a rigid type variable bound by
    the type signature for:
      heteroCompose :: forall (a :: NonEmpty *) (b :: NonEmpty *).
                       Index a -> Index b
    at /home/sandy/prj/tesths/src/Lib.hs:(11,1)-(13,12)
  Expected type: Index b
    Actual type: Index (x ':| xs0)

[isovector]

The solution here is that we shouldn't be able to construct an Index term at all! Because a is a skolem and the only way to construct one is for (x ':| xs) --- which a is not.

[isovector]

My guess then is that this is related to the homo tactic.

[isovector]

Ahh -- homo correctly checks that the domain covers the codomain --- but destructOrHomoAuto doesn't appear to, and that's the one that's called during auto.

[isovector]

So the homo coverage test had a bug in it where I wasn't checking subsetedness. Whoops. But now there's a bug where everything above gets unified to:

heteroCompose
  :: Index a
  -> Index b
heteroCompose (Head x) = x

I think this is because the skolem only gets created when the data constructor is introduced, not when destructing! 😫