SEq vs SDecide, former works better with type checker in certain cases

[infinity0]

(Continued from https://gitlab.haskell.org/ghc/ghc/issues/18035)

Consider the following code, an attempt to implement a heterogeneous association list:

EqVsDecide.hs

```haskell {-# LANGUAGE ConstraintKinds, DataKinds, GADTs, PolyKinds, ScopedTypeVariables, TemplateHaskell, TypeApplications, TypeFamilies, TypeOperators, UndecidableInstances #-} import Data.Kind import Data.Singletons.Decide import Data.Singletons.Prelude import Data.Singletons.TH import Unsafe.Coerce (unsafeCoerce) -- heterogeneous Maybe that carries the type data TMaybe (t :: Maybe k) where TNothing :: TMaybe 'Nothing TJust :: !t -> TMaybe ('Just t) -- heterogeneous assoc list -- kk is separate from vv for easier unification data KVList (kk :: [kt]) (vv :: [Type]) :: Type where KVNil :: KVList '[] '[] KVCons :: !(Sing (k :: kt)) -> !(v :: Type) -> !(KVList kk vv) -> KVList (k : kk) (v : vv) singletons [d| lookupKV :: Eq k => k -> [k] -> [v] -> Maybe v lookupKV k [] [] = Nothing lookupKV k (k':kk) (v:vv) = if k == k' then Just v else lookupKV k kk vv |] hLookupKV :: SEq kt => Sing (k :: kt) -> KVList (kk :: [kt]) vv -> TMaybe (LookupKV k kk vv) hLookupKV sk KVNil = TNothing hLookupKV sk (KVCons sk'' v rem) = case sk %== sk'' of STrue -> TJust v SFalse -> hLookupKV sk rem -- This version doesn't type-check! -- It's similar to the one in the original post, except -- it uses singleton's autogenerated LookupKV type family -- instead of the manually-written one. hLookupKV' :: SDecide kt => Sing (k :: kt) -> KVList (kk :: [kt]) vv -> TMaybe (LookupKV k kk vv) hLookupKV' sk KVNil = TNothing hLookupKV' sk (KVCons sk'' v rem) = case sk %~ sk'' of Proved Refl -> TJust v Disproved _ -> unsafeCoerce (hLookupKV' (unsafeCoerce sk) (unsafeCoerce rem)) -- ^ even unsafeCoerce doesn't help, we are still left with "could not deduce" errors ```

As you can see, the difference between the working and non-working versions are solely down to the choice of SEq vs SDecide. I'm unsure if this is a case of #339, but if it's expected behaviour then perhaps it should be added to the documentation. SEq would seem to fit better into the rest of the singletons framework, and it's unclear what the differences between it and SDecide are, or how their intended use cases differ.

Another thing that is confusing / blocking my understanding, is that the implementation for DefaultEq seems to do the very thing I did at the top of GHC #18035 where we have an overlapping type family declaration, yet somehow it works for singletons. The unsafeCoerce workaround that was cited is only for SEq Type whereas DefaultEq is used for most other types/kinds, it would seem.

[RyanGlScott]

SEq and SDecide, although quite similar, compute two distinct notions of equality. SEq((%==)) computes boolean equality, whereas SDecide((%~)) computes propositional equality. There is a section in the singletons README that highlights some differences between the two.

In the case of your particular program, you are directly using boolean equality in the definition of lookupKV:

  lookupKV k (k':kk) (v:vv) = if k == k' then Just v else lookupKV k kk vv

As a result, you must use boolean equality in order to reduce the if expression. You really do. After all, (==) is an abstract function that has no relationship a priori to the (%~) function. There is no way to know in general that k %~ k' = Proved Refl should imply (k == k') = True for arbitrary k and k'. Similarly, there is no way to know in general that k %~ k' = Disproved _ should imply (k == k') = False.

This isn't a case of #339, since that issue is about internal implementation details leaking through to the user. On the other hand, the use of boolean equality in lookupKV is very much a user-facing detail. This isn't just specific to GHC, either—your version of hLookupKV' won't even typecheck in a language like Idris:

module EqVsDecide

%default total

data TMaybe : Maybe k -> Type where
  TNothing : TMaybe Nothing
  TJust    : t -> TMaybe (Just t)

data KVList : List kt -> List Type -> Type where
  KVNil  : KVList [] []
  KVCons : (k : kt) -> v -> KVList kk vv -> KVList (k::kk) (v::vv)

lookupKV : Eq k => k -> List k -> List v -> Maybe v
lookupKV k [] [] = Nothing
lookupKV k (k'::kk) (v::vv) = if k == k' then Just v else lookupKV k kk vv
lookupKV k _  _  = Nothing

hLookupKV : Eq kt => (k : kt) -> KVList kk vv -> TMaybe (lookupKV k kk vv)
hLookupKV k KVNil = TNothing
hLookupKV k (KVCons k' v r) with (k == k')
  hLookupKV k (KVCons k' v r) | True  = TJust v
  hLookupKV k (KVCons k' v r) | False = hLookupKV k r

hLookupKV' : (DecEq kt, Eq kt) => (k : kt) -> KVList kk vv -> TMaybe (lookupKV k kk vv)
hLookupKV' k KVNil = TNothing
hLookupKV' k (KVCons k' v r) with (decEq k k')
  hLookupKV' k (KVCons k v r)  | Yes Refl = TJust v
  hLookupKV' k (KVCons k' v r) | No _     = hLookupKV' k r

$ idris --check EqVsDecide.idr
EqVsDecide.idr:27:45-51:
   |
27 |   hLookupKV' k (KVCons k v r)  | Yes Refl = TJust v
   |                                             ~~~~~~~
When checking right hand side of with block in EqVsDecide.hLookupKV' with expected type
        TMaybe (if k == k then Just v else lookupKV k kk vv)

Type mismatch between
        TMaybe (Just v) (Type of TJust v)
and
        TMaybe (if k == k then Just v else lookupKV k kk vv) (Expected type)

Specifically:
        Type mismatch between
                Just v
        and
                if k == k then Just v else lookupKV k kk vv

Notice that Idris is unable to reduce k == k, as that would require extra information about the laws of boolean equality that aren't expressed in the types. If Idris can't figure this out, then I don't think there's any hope for GHC :)

[infinity0]

OK, thanks I can appreciate that they are distinct concepts and can't be mixed. I'm guessing that "boolean equality" means "related to the Eq class and its promoted variants" and "propositional equality" means "from the viewpoint of the GHC / Haskell type checker attempting unification", hopefully this is an accurate of putting it? So in theory if singletons, when promoting if k == k' then .. else .., translated it to something involving SDecide instead of PEq and SEq, then I would have to use a SDecide constraint in hLookupKV, is that right?

Does that feature even make sense? As I understand, it's not possible in Haskell to declare that two term-level variables are equal, but on the type-level we can do this, so singletons could theoretically translate this to propositional instead of boolean equality. (I'm not asking for the feature, I don't have an immediate use for it; I'm just trying to confirm my understanding by predicting something.) Then unsafeCoerce should hopefully still be unnecessary, because we are avoiding GHC #18035 by using the singletons-promoted If.

(I did not try doing this manually yet, as I don't know what the promoted analogue of SDecide would be, like how we have PEq and SEq.)

If my understanding based on your explanation is correct, then having LookupKV be redefined in terms of If is the real reason behind being able to avoid unsafeCoerce. This SEq vs SDecide issue is just a side consequence of using If and how singletons promotes if k == k' then .. else .., so it can be closed since it is effectively a duplicate of GHC #18053.

[RyanGlScott]

I'm guessing that "boolean equality" means "related to the Eq class and its promoted variants" and "propositional equality" means "from the viewpoint of the GHC / Haskell type checker attempting unification", hopefully this is an accurate of putting it?

Boolean equality is a simple form of equality that checks if two things are equal and returns a simple "yes" or "no" answer (i.e., a Bool). Propositional equality (or, if you want to be pedantic, decidable propositional equality) returns a "yes" or "no" answer with extra information. If it answers "yes", then it also provides evidence that the two things are equal (i.e., a :~: b). If it answers "no", then it also provides evidence that assuming the two things are equal would lead to a contradiction (i.e., a :~: b -> Void).

Eq and SDecide are two particular ways of computing boolean and propositional equality, respectively, in Haskell. This is not say that they are the only ways of computing these notions of equality. (See, for instance, the Boolean and dec libraries, which provide alternative takes on boolean and propositional equality, respectively.)

So in theory if singletons, when promoting if k == k' then .. else .., translated it to something involving SDecide instead of PEq and SEq, then I would have to use a SDecide constraint in hLookupKV, is that right?

Short answer: there is no easy way to promote if k == k' then .. else .. to the type level, since SDecide does not have a promoted counterpart for various reasons.

Long answer: To see if what you describe is possible, let's go back to the Idris version of the program. We can define a variant of lookupKV that uses DecEq (Idris' equivalent of SDecide) instead of Eq:

lookupKV : DecEq k => k -> List k -> List v -> Maybe v
lookupKV k [] [] = Nothing
lookupKV k (k'::kk) (v::vv) with (decEq k k')
  lookupKV k (k ::kk) (v::vv) | Yes Refl = Just v
  lookupKV k (k'::kk) (v::vv) | No  _    = lookupKV k kk vv
lookupKV k _  _  = Nothing

Having done this, if we then define hLookupKV' to use DecEq:

hLookupKV' : DecEq kt => (k : kt) -> KVList kk vv -> TMaybe (lookupKV k kk vv)
hLookupKV' k KVNil = TNothing
hLookupKV' k (KVCons k' v r) with (decEq k k')
  hLookupKV' k (KVCons k v r)  | Yes Refl = TJust v
  hLookupKV' k (KVCons k' v r) | No _     = hLookupKV' k r

Then it typechecks! This good news, since making this program work a language with native support for dependent types hints at the possibility that we could encode it with singletons. But we shouldn't celebrate too quickly, since it's not possible to just do this:

$(singletons [d|
  lookupKV :: Decide k => k -> [k] -> [v] -> Maybe v
  lookupKV k [] [] = Nothing
  lookupKV k (k':kk) (v:vv) =
    case k %~ k' of
      Proved Refl -> Just v
      Disproved _ -> lookupKV k kk vv
  |])

There are numerous problems with this idea, but the most notable problem is that we can't define a "simply typed" version of (%~) that doesn't involve Sings. The type of (%~) requires dependent function types, which Sing emulates. This means that the likelihood of making this Just Work™ using nothing but Template Haskell is almost zero.

That being said, we might be able to accomplish this if we are willing to get our hands dirty. First, we need to define a PDecide class with a type-level version of (%~):

class PDecide k where
  type (a :: k) :~ (b :: k) :: PDecision (a :~: b)

(I'll define PDecision momentarily.)

While GHC doesn't have full-spectrum dependent types, it does have visible dependent quantification at the kind level. Note that the full kind of (:~) is: forall k. forall (a :: k) (b :: k) -> PDecision (a :~: b)—we don't need Sings to have dependent functions in kinds!

The next step is to change SDecide so that it is expressed in terms of PDecide. In other words, define SDecide like so:

class SDecide k where
  (%~) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Sing (a :~ b)

In order to make that work, we'll need a singled version of Decision. Let's define that now:

data (%:~:) :: forall a b. a :~: b -> Type where
  SRefl :: (%:~:) Refl
type instance Sing = (%:~:)

data Decision' p a
  = Proved a
  | Disproved (p @@ a @@ Void)
type Decision  = Decision' (TyCon2 (->))
type PDecision = Decision' (~>@#@$)

data SDecision :: forall a. PDecision a -> Type where
  SProved    :: forall a (x :: a).         Sing x -> SDecision (Proved x)
  SDisproved :: forall a (r :: a ~> Void). Sing r -> SDecision (Disproved r)
type instance Sing = SDecision

(Note that I'm using a trick from #82 to allow Decision to have a field of type a -> Void and PDecision to have a field of type a ~> Void.)

With this out of the way, we can now define a version of LookupKV that uses propositional equality:

type family LookupKV (a :: k) (as :: [k]) (bs :: [v]) :: Maybe v where
  LookupKV k '[] '[]        = Nothing
  LookupKV k (k':kk) (v:vv) = Case k k' (k :~ k') kk v vv

type family Case (a :: k) (a' :: k) (pd :: PDecision ((a :: k) :~: a')) (as :: [k])
                 (b :: v) (bs :: [v]) :: Maybe v where
  Case k k  (Proved Refl) kk v vv = Just v
  Case k k' (Disproved _) kk v vv = LookupKV k kk vv

And finally, a version of hLookupKV' that uses SDecide:

hLookupKV'
  :: SDecide kt
  => Sing (k :: kt)
  -> KVList (kk :: [kt]) vv
  -> TMaybe (LookupKV k kk vv)
hLookupKV' sk KVNil = TNothing
hLookupKV' sk (KVCons sk'' v rem) = case sk %~ sk'' of
  SProved SRefl -> TJust v
  SDisproved _  -> hLookupKV' sk rem

Phew, that was a lot of work! But this does demonstrate that all of this is technically possible. The tricky part, then, is figuring out how you might get Template Haskell to generate all of this code:

1. The kind of LookupKV uses visible dependent quantification. Currently, the TH defunctionalization machinery doesn't play nicely with visible dependent quantification—see here.
2. Generating Decision' with Template Haskell would require a fix for #82.
3. Generating a Sing instance for (:~:), a GADT, would require a fix for #150.

My belief is that we're a long ways away from accomplishing this. For these reasons, I think it's best to stick to the simpler version of SDecide that singletons currently provides.

[infinity0]

Thank you very much for that detailed explanation and expansion! That confirms what I thought I understood from your previous comments. I can certainly understand that doing this automatically in TH is a long way off, and am in no hurry to want this potential feature.

PDecide et.al. all make sense, I was wondering if they already existed in some other form already. I suppose you can best decide if it would be good to add it in even if no autogeneration support in TH exists for it - it would bring SDecide up to a similar feature-level as the autogenerated Prelude types, though I appreciate this is just a toy example and you did mention there were various other reasons this did not exist already.

[RyanGlScott]

It's not unheard of to implement certain definitions in singletons by hand. (See, for instance, the Data.Singletons.TypeError module, which is mostly written from scratch for various reasons.) But if we're going to add another hand-written thing to singletons, there had better be good reasons for doing so. I'm not entirely convinced that PDecide would be a useful addition on its own, but I could be convinced otherwise if there is enough demand for it.

[infinity0]

I may have just found a use case for it. Suppose we want to do something based on a runtime value, we can use withSomeSing but then %== doesn't type-check:

{-# LANGUAGE DataKinds, GADTs, KindSignatures, ScopedTypeVariables, TypeApplications #-}

import           Data.Text (pack)
import           Data.Singletons.Decide
import           Data.Singletons.Prelude
import           Data.Singletons.TypeLits

main = do
  let k0 = SSym @"a"
  withSomeSing (pack "a") $ \(k :: Sing (kt :: Symbol)) -> do
    {-case k0 %== k of
      STrue -> print "yes" -- error: ‘a0’ is untouchable inside the constraints: DefaultEq "a" a ~ 'True
      SFalse -> print "no" -- similar error -}
    case k0 %~ k of
      Proved Refl -> print "yes"
      Disproved _ -> print "no"

This also affects the other code I've been writing - the proof-constraints cannot be satisfied inside a withSomeSing for the same reasons, resulting in similar error messages, because the type-variable representing the value is not touchable. It would seem that only %~ provides us this information dynamically at runtime - I didn't immediately realise that this was a consequence of the definition when I first heard it. So to support this feature in my code, I suppose I'd have to re-write everything to use SDecide instead of SEq, including manually promoting everything like you did above. :(

Or is there another way of doing this with SEq? I wouldn't be surprised, I'm still in the learning phase...

[RyanGlScott]

That's just due to a limitation of GHC's type inference, I believe. It will typecheck if you add a type signature to main:

main :: IO ()
main = do
  let k0 = SSym @"a"
  withSomeSing (pack "a") $ \(k :: Sing (kt :: Symbol)) -> do
    case k0 %== k of
      STrue  -> print "yes"
      SFalse -> print "no"

[infinity0]

Ah, it turns out I had a signature, but I was testing my example by commenting out only the %== case. If you have two cases, you also need to supply an explicit type signature to the first case, GHC is only able to infer the type for the second case.

main :: IO ()
main = do
  let k0 = SSym @"a" :: Sing ("a" :: Symbol)
  --let k = SSym @"b"
  withSomeSing (pack "a") $ \(k :: Sing (kt :: Symbol)) -> do
    (case k0 %== k of
      STrue -> print "yes"
      SFalse -> print "no") :: IO ()  -- explicit type signature needed...
    case k0 %~ k of
      Proved Refl -> print "yes"
      Disproved _ -> print "no"

---

That was a red herring; the real problem I was having, is that if your proofs rely on PEq (as mine did), which is likely if your functions use Eq and SEq, then inside a withSomeSing GHC can't apply the type-family DefaultEq when solving constraints. Here is a minimal example, it behaves slightly differently from my big example but it captures a similar sort of weirdness:

class Wf k kk where
instance Wf k '[]
instance (Vf (k == k1)) => Wf k (k1 ': kk)

class Vf eq where
instance Vf 'True
instance Vf 'False

vf :: Vf (k == k1) => Sing k -> Sing k1 -> IO ()
vf k k' = pure ()

wf :: Wf k kk => Sing k -> Sing kk -> IO ()
wf k k' = pure ()

main :: IO ()
main = do
  let k0 = SSym @"a" :: Sing ("a" :: Symbol)
  let kk = sing :: Sing ('["a" :: Symbol])
  vf k0 k0 >> wf k0 kk
  withSomeSing (pack "a") $ \(k :: Sing (kt :: Symbol)) -> do
    -- vf k0 k -- No instance for (Vf (DefaultEq "a" a)) arising from a use of ‘vf’
    -- vf k k0 -- No instance for (Vf (DefaultEq a "a")) arising from a use of ‘vf’
    -- wf k kk -- No instance for (Vf (DefaultEq a "a")) arising from a use of ‘wf’
    -- potential workarounds below:
    (_ :: ()) <- case k %== k0 of
      STrue -> vf k k0 >> wf k kk
      SFalse -> vf k k0 >> wf k kk
    (_ :: ()) <- case k0 %== k of -- note, only difference is order of comparison
      STrue -> vf k0 k -- vf k k0 >> wf k kk -- Could not deduce (Vf (DefaultEq a "a"))
      SFalse -> vf k0 k -- vf k k0 >> wf k kk -- Could not deduce (Vf (DefaultEq a "a"))
    case k0 %~ k of
      Proved Refl -> vf k0 k >> vf k k0 >> wf k kk
      Disproved _ -> pure () -- vf k0 k >> vf k k0 >> wf k kk -- No instance for (Vf (DefaultEq "a" a))
    case k %~ k0 of
      Proved Refl -> vf k0 k >> vf k k0 >> wf k kk
      Disproved _ -> pure () -- vf k0 k >> vf k k0 >> wf k kk -- No instance for (Vf (DefaultEq "a" a))

Perhaps you can understand the behaviour a bit better; my current guess at understanding it is that, one can recover enough types for GHC to deduce the constraints, by applying runtime functions involving Sing then pattern-matching on the results, but you have to do this in the same way as the "shape" of the implementation of the original constraint-based proofs otherwise GHC can't perform the deductions. I'm not sure if this is really correct though, it would be more obvious if GHC could print out its deduction steps but I haven't seen a compiler flag for that yet...

This would seem to put a dampener on the whole technique of encoding proofs as constraints - if you want resolution based on runtime types that is; so I suppose the fix will have to involve encoding proofs using the runtime Sing values. Do you have some examples for that? I did not see examples in singletons itself of passing theorems around, and the example at the top of #339 is a bit opaque for a dependent-types newbie like myself.

---

Separately and before I realised the above, I attempted to fix it by building on top of your PDecide code and got stuck, specifically:

instance PDecide Symbol where
  type a :~ a = 'Proved 'Refl
  -- Expected kind ‘((~>@#@$) @@ (a :~: b)) @@ Void’
  -- we want to find constructors with type ((a :~: b) ~> Void) then promote it to the kind level
  -- but TyFun / (~>) do not have constructors
  type a :~ b = 'Disproved {-- what goes here? --}

Not sure if this is just because of the fact that your code was a toy example, or because of my missing knowledge about the library. Anyway after the above reasoning, I believe even if this worked, it wouldn't actually fix my problem since it's unrelated to how the constraints are being resolved.

By the way, thank you for being patient with all of my questions which might seem a bit basic. I hope this discussion will be useful for other people - I am trying to do some stuff that is a bit more complex than the typical basic tutorials on dependent types, but that is fairly reasonable and intuitively-desired for "real world" use cases I think, so hopefully this brings us all some experience on how to communicate about these languages & techniques better to more people.

[RyanGlScott]

At the risk of sounding like a broken record, the type errors you're experiencing are just a symptom of GHC's inability to perform type inference underneath GADT pattern matches. In particular, GHC is reluctant to infer types underneath equality constraints. Here is a very small example from Section 5.1 of the paper OutsideIn(X), which is the standard reference for how GADT type inference works:

{-# LANGUAGE GADTs #-}
module Foo where

data T a where
  T1 :: Int -> T Bool

f = \x -> case x of { T1 n -> n > 0 }

Like several of your prior examples, this will fail to typecheck:

Foo.hs:7:31: error:
    • Couldn't match expected type ‘p’ with actual type ‘Bool’
        ‘p’ is untouchable
          inside the constraints: a ~ Bool
          bound by a pattern with constructor: T1 :: Int -> T Bool,
                   in a case alternative
          at Foo.hs:7:23-26
      ‘p’ is a rigid type variable bound by
        the inferred type of f :: T a -> p
        at Foo.hs:7:1-37
      Possible fix: add a type signature for ‘f’
    • In the expression: n > 0
      In a case alternative: T1 n -> n > 0
      In the expression: case x of { T1 n -> n > 0 }
    • Relevant bindings include f :: T a -> p (bound at Foo.hs:7:1)
  |
7 | f = \x -> case x of { T1 n -> n > 0 }
  |                               ^^^^^

The difficulty here is that f does not have a most general type. It could conceivably be given the types T a -> a or T a -> Bool, but neither type is more general than the other. Basically all "untouchble" errors have a similar flavor. And all of them can be fixed by adding more type signatures. That's really all there is to it, I'm afraid!

This is not to say that GHC cannot perform any type inference under GADT pattern matches. Section 5.1 of OutsideIn(X) also makes a note of this example which GHC is able to infer a type for:

{-# LANGUAGE GADTs #-}
module Foo where

data T a where
  T1 :: Int -> T Bool
  T2 :: T a

-- g :: T a -> Bool
g = \x -> case x of { T1 n -> n > 0; T2 -> True }

This time, T a -> Bool actually is the most general type (since it cannot be given the type T a -> a), so GHC infers it. This is why some of your examples happen to typecheck—due to the way constraint solving works, GHC is sometimes clever enough to notice when the set of equality constraints leads to a most general type.

Personally speaking, I find this constraint solving process difficult to predict, so I almost always err on the side of giving explicit type signatures. Sometimes, this means breaking things up into smaller pieces:

main :: IO ()
main = do
  let k0 = SSym @"a"
  withSomeSing (pack "a") $ \(k :: Sing (kt :: Symbol)) -> do
    let step1 :: IO ()
        step1 =
          case k0 %== k of
            STrue -> print "yes"
            SFalse -> print "no"

        step2 :: IO ()
        step2 =
          case k0 %~ k of
            Proved Refl -> print "yes"
            Disproved _ -> print "no"

    step1
    step2

if you want resolution based on runtime types that is; so I suppose the fix will have to involve encoding proofs using the runtime Sing values. Do you have some examples for that? I did not see examples in singletons itself of passing theorems around, and the example at the top of #339 is a bit opaque for a dependent-types newbie like myself.

I'm not quite sure what you mean by "passing theorems around".

Separately and before I realised the above, I attempted to fix it by building on top of your PDecide code and got stuck, specifically:

instance PDecide Symbol where
  type a :~ a = 'Proved 'Refl
  -- Expected kind ‘((~>@#@$) @@ (a :~: b)) @@ Void’
  -- we want to find constructors with type ((a :~: b) ~> Void) then promote it to the kind level
  -- but TyFun / (~>) do not have constructors
  type a :~ b = 'Disproved {-- what goes here? --}

We can take inspiration from the current SDecide Symbol instance, which is defined like so:

https://github.com/goldfirere/singletons/blob/779b8ccdb7cf8746fbe01ea521e035dd69e7aa64/src/Data/Singletons/TypeLits/Internal.hs#L97-L103

singletons takes the easy way out and just uses error. This is a bit strange, but then again, sameSymbol is defined in terms of unsafeCoerce, so it's far from the strangest thing going on here. The implementation of (%~) suggests one possible way to define a PDecide Symbol instance:

$(singletons [d|
  disprovedSymbol :: a :~: b -> Void
  disprovedSymbol _ = error "Broken Symbol singletons"
  |])

type family DecideSymbol (a :: Symbol) (b :: Symbol) :: PDecision (a :~: b) where
  DecideSymbol a a = Proved Refl
  DecideSymbol a b = Disproved DisprovedSymbolSym0

instance PDecide Symbol where
  type a :~ b = DecideSymbol a b

instance SDecide Symbol where
  (SSym :: Sing n) %~ (SSym :: Sing m)
    | Just Refl <- GHC.TypeLits.sameSymbol (Proxy :: Proxy n) (Proxy :: Proxy m)
    = SProved SRefl
    | otherwise
    = unsafeCoerce $ SDisproved (singFun1 @DisprovedSymbolSym0 sDisprovedSymbol)

[infinity0]

Sorry, I don't think my problem was the lack of type signatures, I really did add plenty already. But I think I've figured out the problem in the meanwhile, here is the solution:

In the example over in #339 I encoded a proof as a constraint, of (fmap f (lookupKV k kk vv) == lookupKV k kk (fmap f vv))

How this proof works is by induction, but when GHC actually comes to selecting an instance, it steps through the proof with the type variables instantiated to real types. Intuitively speaking, it "runs" the proof for a single case, it doesn't prove the proof for all cases.

This doesn't work if the type is a runtime type like (DefaultEq a "a") with an unknown/untouchable type variable a, GHC cannot fully resolve this type family application into a type, it gets "stuck". So it fails selecting an instance. Even if all possible RHS of the type family application (in this case, 'STrue and 'SFalse) would allow an instance to be selected, GHC by design has to select an actual instance at compile-time not at run-time, and so it fails.

To make this work, one has to do a case-match underneath a %==. This is OK if your computed type only involves one use of PEq, however in my proof in the example code we are fmapping over all keys in a container. (I tried to capture this recursion in the fake version of Wf a few comments above but I guess you overlooked that, understandly.) So in our code, we have to do a run-time case-match on all the %== comparisons before we can use the type concretely and it becomes touchable.

This was where I got stuck yesterday, but I realised that you can write a recursive witheSomeWf function similar to withSomeSing to perform all of these %== matches to bring the Wf proof constraint into scope, and now my code works. This was something that was not immediately obvious from Stephanie's examples - the proof is not (easily) usable with runtime types unless you also provide this accompanying utility function. I am not sure if this sort of pattern is conventional in Agda/Idris, maybe you can shed some light on that?

Continuing from the example over in #339:

-- | Prove @Wf f k kk vv@. You need this inside a @withSomeSing@ and other
-- similar constraints involving a runtime 'k', in order to bring the
-- @Wf f k kk vv@ constraint into scope, to use certain utility functions like
-- 'withLookupKV' that require this constraint, representing a theorem.
withSomeWf
  :: forall f (k :: kt) (kk :: [kt]) vv r
   . SEq kt
  => Proxy f
  -> Sing k
  -> KVList kk vv
  -> (Wf f k kk vv => r)
  -> r
withSomeWf _ k KVNil c = c
withSomeWf p k (KVCons k' v tab) c = case k %== k' of
  STrue -> withSomeWf p k tab c
  SFalse -> withSomeWf p k tab c

main :: IO ()
main = do
  let v = KVCons (SSym @"a") (3 :: Int)              $ KVCons (SSym @"b") "test"     $ KVNil
  let c = KVCons (SSym @"a") (show . (+) (2 :: Int)) $ KVCons (SSym @"b") (<> "ing") $ KVNil
  let k0 = SSym @"a"
  let k1 = SSym @"b"
  void $ traverse print $ withLookupKV v k0 c
  withSomeSing (pack "a") $ \k -> do
    -- without this line, GHC fails with:
    -- No instance for (Vf (FlipSym2 (TyCon2 (->)) [Char]) {..etc..} (DefaultEq a "a"))
    --   arising from a use of ‘withLookupKV’
    withSomeWf (Proxy @(FlipSym2 (TyCon2 (->)) [Char])) k v $ do
      void $ traverse print $ withLookupKV v k c

(And yes, later I'll probably switch on AllowAmbiguousTypes to avoid the Proxy instances.)

I'm not quite sure what you mean by "passing theorems around".

I thought that a solution might require passing some term around that represents the proof, and then each function would case-match on this term to bring the proof into scope. The solution above uses the "with-continuation" pattern instead, which is nicer since it only has to be used once, and no term-level proofs are needed. This alternative technique might have some advantages such as avoiding the constraint solver and its slightly opaque error messages, although I did not try it yet because it's not clear to me how to encode Wf/Vf inside a GADT.

I think this covers all of my use-cases, so hopefully I won't have any more questions! Thanks for all your help so far. I will try to write all of this up at some point as a guide for anyone else trying to do similar things.

[RyanGlScott]

Sorry, I don't think my problem was the lack of type signatures, I really did add plenty already.

My apologies. There have been a multitude of examples discussed in this issue, so I likely had a different example in mind than the one you were referring to. (The examples in https://github.com/goldfirere/singletons/issues/447#issuecomment-612625294 definitely suffered from a lack of type signatures.)

This was where I got stuck yesterday, but I realised that you can write a recursive witheSomeWf function similar to withSomeSing to perform all of these %== matches to bring the Wf proof constraint into scope, and now my code works. This was something that was not immediately obvious from Stephanie's examples - the proof is not (easily) usable with runtime types unless you also provide this accompanying utility function. I am not sure if this sort of pattern is conventional in Agda/Idris, maybe you can shed some light on that?

I don't think I'm experienced enough in either Agda or Idris to say with certainty whether encoding proofs as implicit arguments is "conventional" or not. I do know that type class resolution works differently in Haskell than in languages like Agda/Idris, since the former enforces global coherence of class instances, while the latter do not. That doesn't necessarily mean that it's impossible to write implicit-arguments-as-proofs–style code in these languages, but the ergonomics might be different.

I thought that a solution might require passing some term around that represents the proof, and then each function would case-match on this term to bring the proof into scope.

I suppose it depends on your perspective. If you look at the implementation of withSomeWf, you'll notice that it still carries out all of the key steps of the proof. It proceeds by cases (i.e., pattern matches) on the constructors of KVList, and in the KVCons case, it must proceed by cases on whether k equals k' before applying the inductive hypothesis (i.e., recursing). So there is still term-passing and case-matching going on your program, but the presentation is slightly different due to the use of type classes.

I think this covers all of my use-cases, so hopefully I won't have any more questions!

Wonderful! Does this mean that this issue can be closed?

[infinity0]

Sounds good, there is nothing actionable on the singletons library here. Perhaps later I will come up with some documentation suggestions.