Wingman is still flummoxed by GADT evidence

[isovector]

{-# LANGUAGE DataKinds #-}

import Data.Kind

data Nat = Z | S Nat

data HList (ls :: [Type]) where
  HNil :: HList '[]
  HCons :: t -> HList ts -> HList (t ': ts)

data ElemAt (n :: Nat) t (ts :: [Type]) where
  AtZ :: ElemAt 'Z t (t ': ts)
  AtS :: ElemAt k t ts -> ElemAt ('S k) t (u ': ts)

lookMeUp :: ElemAt i ty tys -> HList tys -> ty
lookMeUp AtZ (HCons t' hl) = _
lookMeUp (AtS ea') (HCons _ hl') = lookMeUp ea' hl'

Wingman should be able to fill in the hole with t'. GHC knows this:

 Found hole: _ :: ty
• Relevant bindings include
    hl :: HList ts1 (bound at /home/sandy/prj/tesths/src/Lib.hs:19:24)
    t' :: t (bound at /home/sandy/prj/tesths/src/Lib.hs:19:21)
    lookMeUp :: ElemAt i ty tys -> HList tys -> ty
      (bound at /home/sandy/prj/tesths/src/Lib.hs:19:1)
  Constraints include
    tys ~ (t : ts1) (from /home/sandy/prj/tesths/src/Lib.hs:19:15-25)
    i ~ 'Z (from /home/sandy/prj/tesths/src/Lib.hs:19:10-12)
    tys ~ (ty : ts) (from /home/sandy/prj/tesths/src/Lib.hs:19:10-12)

We can learn this by unifying (t : ts1) ~ tys ~ (ty : ts) therefore t ~ ty and ts1 ~ ts. But that information never makes it to the Wingman unifier. Instead, our substition set looks like:

   In scope: InScope {t ts}
   Type env: [a1fDf :-> (':) @* t ts, a1fDk :-> t, a1fDl :-> ts]
   Co env: []]
!!!subst: [TCvSubst
   In scope: InScope {ty ts}
   Type env: [a1fDe :-> ty, a1fDf :-> (':) @* ty ts, a1fDh :-> ts]
   Co env: []]
!!!subst: [TCvSubst In scope: InScope {} Type env: [a1fDd :-> 'Z] Co env: []]

The relevant bits here are the substitutions of a1fDf :-> (':) @* ty ts and a1fDf :-> (':) @* t ts. But it's weird --- two separate substitutions for the same variable? Is this substitution not being persisted somehow?

[isovector]

Digging in deeper, this is the evidence we've got: [EqualityOfTypes i 'Z,EqualityOfTypes tys (ty : ts),EqualityOfTypes tys (t : ts)] which is absolutely right. So I think the issue is that we're not applying the substitution to the evidence.