Is :> too rigid?

[jwiegley]

I'm trying to figure out how to get the following to work:

stronger :: f :< r => Sum r v -> a
stronger = undefined

weaker :: f :< r => Sum (e ': r) v -> a
weaker = stronger

I would think that f :> r entails the constraint f :> any ': r, but this does not seem to be the case. Intuitively I would see the entailment as just a Succ on the former witness. Instead, the error I get is:

• Could not deduce (KnownNat (ElemIndex f0 (e : r)))
    arising from a use of ‘stronger’
  from the context: f :< r
    bound by the type signature for:
               weaker :: forall (f :: * -> *) (r :: [* -> *]) (e :: * -> *) v.
                         (f :< r) =>
                         Sum (e : r) v -> f v
    at /Users/johnw/src/trade-journal/src/Journal/SumLens.hs:74:1-41
  The type variable ‘f0’ is ambiguous
  Relevant bindings include
    weaker :: Sum (e : r) v -> f v
      (bound at /Users/johnw/src/trade-journal/src/Journal/SumLens.hs:75:1)

[jwiegley]

Seems to be the possibility that f ~ any that breaks it. If I had a type inequality between the two, then I should be able to influence the type checker to "look in the tail"...

[jwiegley]

Apologies for the issue churn. I tried getting more specific with the types, and found that this still fails:

stronger :: f :< r => Sum r v -> a
stronger = undefined

weaker :: Const Int :< r => Sum (Const Double ': r) v -> f v
weaker = stronger @(Const Int)

However, if I replace Element with Oleg's formulation, the same code works:

class Element (t :: * -> *) r where
  elemNo :: P t r

instance Element t (t ': r) where
  elemNo = P 0

instance Element t r => Element t (t' ': r) where
  elemNo = P $ 1 + (unP $ (elemNo :: P t r))

I wonder if it can be made to work also with the ElemIndex magic?

[jwiegley]

I've also found that (Const Int :< r, r :<: s) is insufficient to entail that Const Int :< s, which it seems should follow?

[patrickt]

Yeah, this is the problem with ElemIndex—it's a loop unrolled in the type system, so GHC goes quickly but loses, for reasons that I'll admit are not wholly clear to me, some invariants that should still hold. I think @robrix hit this once.

[patrickt]

For the example of (Const Int :< r, r :<: s), there not being an instance for Const Int :< s kind of makes sense, because I don’t think the type checker can be expected to infer that the presence of both these judgments, across :< and :<:), can entail a further judgment across (for some value of “across”, I don’t know the term of art here) them.

[patrickt]

Looking at the Oleg’s example, that’s exactly where ElemIndex falls down, I’m afraid. The abstraction is actually very simple: if it were cleaned up and written by hand, it would look like this:

type family ElemIndex (t :: * -> *) (ts :: [* -> *]) :: Nat where
  ElemIndex t [t] = 0
  ElemIndex t [_, t] = 1
  ElemIndex t [_, _, t] = 2

And so on and so forth, all up to 150. The act of recurring has been unrolled away, so there’s no application of a Succ constructor. Maybe if we used a hand-rolled Succ instead of Nat? But it’s hard to imagine that wouldn’t hurt speed at high arities. so that’s out.

[robrix]

I think this is another instance of non-inductive hypotheses biting us. The right solution is for the ghc issue(s) to be resolved, obviating the need for fastsum altogether. I live in hope…