[#6] Implement dipT using dipN and dupT using dupN

added 1 commit

11a75197 - fixup! [#6 (closed)] Implement dipT using dipN

marked this merge request as draft from 11a75197

@pasqu4le This is not quite what I was hoping for, and I think not what you really wanted either. The approach I thought prettiest was something like this:

instance ( dipInp ~ (a ': tlDI)
         , index ~ ToPeano (TheOnly (StackElemNotFound inp a)
                                    (StackElemAmbiguous inp a)
                                    (FindIndices (DefaultEqSym1 a) inp))
         , ConstraintDIPNLorentz index inp out dipInp dipOut
         ) =>
  DipT a inp dipInp dipOut out where
  dipT = dipNPeano @index

type family TheOnly (empty_err :: ErrorMessage) (many_err :: ErrorMessage) (xs :: [k]) :: k where
  TheOnly e_err _ '[] = TypeError e_err
  TheOnly _ _ '[x] = x
  TheOnly _ m_err _ = TypeError m_err

For reasons I don't understand, this goes quite horribly wrong when an error gets triggered—each error report is duplicated numerous times (with exactly the same text and location info) and splatted out all over the terminal. I haven't tried to see if that will change with a later version of GHC.

My next attempt was to get rid of the dipT' method, using the DipT' class only to guide inference and adding a ConstraintDIPNLorentz instance constraint to DipN. This went much better, but it still has a bit of an error reporting problem. ConstraintDIPNLorentz requires ConstraintDIPN, which in turn attempts to do its own "fancy" error reporting using RequireLongerOrSameLength. But the way that's defined causes it to throw an insufficient length error whenever it can't determine whether the length is sufficient. The result is that we end up both with the error we want and a (rather mysterious) error relating to internals.

Specifically, we have

type family RequireLongerOrSameLength' (l :: [k]) (a :: Peano) :: Constraint where
  RequireLongerOrSameLength' l a =
    If (IsLongerOrSameLength l a)
       (() :: Constraint)
       (TypeError
          ('Text "Expected stack with length >= " ':<>: 'ShowType (FromPeano a) ':$$:
           'Text "Current stack has size of only " ':<>:
           'ShowType (LengthWithTail l) ':<>:
           'Text ":" ':$$: 'ShowType l
           ))

When IsLongerOrSameLength l a is stuck, the If type family will be stuck as well. Since one of the arguments is a TypeError, that error will be reported (even though it doesn't really make much sense in context).

One option would be to redefine RequireLongerOrSameLength':

type RequireLongerOrSameLength' (l :: [k]) (a :: Peano) = RequireLongerOrSameLength'' l a (IsLongerOrSameLength l a)
type family RequireLongerOrSameLength'' (l :: [k]) (a :: Peano) (lngr :: Bool) :: Constraint where
  RequireLongerOrSameLength'' _ _ 'True = ()
  RequireLongerOrSameLength'' l a 'False =
        (TypeError
          ('Text "Expected stack with length >= " ':<>: 'ShowType (FromPeano a) ':$$:
           'Text "Current stack has size of only " ':<>:
           'ShowType (LengthWithTail l) ':<>:
           'Text ":" ':$$: 'ShowType l
           ))

Now a stuck length comparison won't trigger a length error, and we'll only get the error we want. The potential downside is that if a user is using dipN directly, and encounters a stuck type, their error message will refer to RequireLongerOrSameLength'', which isn't really any of their business.

Another approach might be to separate out the RequireLongerOrSameLength from ConstraintDIPN, so we can have one version of dipN that does fancy error business and another version (more appropriate for use in libraries) that does not. I don't love the duplications inherent in this (spread across the API), but I think it may remove a lot of confusing-error headaches.

Ok, I must admit that I'm lost and I don't really know what's happing.

I tried several approaches with type families as well, mostly using variations of this:

instance
  ConstraintDIPNLorentz (IsOnlyAt a inp 'Z) inp out dipInp dipOut
  => DipT a inp dipInp dipOut out where
  dipT = dipNPeano @(IsOnlyAt a inp 'Z)

type family IsOnlyAt (a :: k) (l :: [k]) (n :: Peano) :: Peano where
  IsOnlyAt _ '[] _ = TypeError ('Text "none")
  IsOnlyAt a (a ': as) n = If (IsElem a as) (TypeError ('Text "multiple")) n
  IsOnlyAt a (_ ': as) n = IsOnlyAt a as ('S n)

which works without DipT' and satisfies the fundeps too (not the class constrait, but that can be added).

The problem is that, just like you, in case typechecking fails I get a repeated compilation error. Which is a shame because otherwise I would have liked to go with this or something similar.

As much as I tried to turn this around and try to localize the source of it, I'm still not sure what's causing the repeated error, which seems to happen consistently too (e.g. if I change the Natural in _dipSample1 for another type it always results in 13 prints of the error, no matter what I do).

Most worryingly I was hoping that it was possible to force the order of resolution of the constraints and type families by using Ifs, but then it happened that this:

type ConstraintDipT a inp dipInp dipOut out =
  If (IsElem a inp)
     (ConstraintDIPNLorentz (IsOnlyAt a inp 'Z) inp out dipInp dipOut)
     (TypeError ('Text "none1"))

doesn't even compile on it's own ... yes, I get a type error on the type synonym itself

So now I'm really starting to thing that there's a bug in GHC perhaps

I think that, unless we find the cause or that it's indeed a bug already solved, a solution like this is not applicable and we'll need to fall back to the one in !1197 (closed)

I haven't spent as much time on your second attempt, but it seems to me that we'd have to accept exposing the user to internals, unrelated (as far as they know) error messages or take apart the tree of constraints that is ConstraintDIPNLorentz to use it here (with considerable duplication, as you pointed out). I don't like either of these outcomes, I'd say that also in this case it would be more sensible to fall back to !1197 (closed).

Does your type synonym compile when it's changed to a type family?

Yep, it does compile when it's a type family.

However I still can't use the it as-is as as the only constraint for a dipT function because the result is that GHC can't figure out:

Expected stack with length >= FromPeano (IsOnlyAt a0 inp 'Z)

And, just as oddly, this error is also reported twice

I played around with it a bit, but I cannot seem to obtain any other result but either of these two.

Adam Gundry made a suggestion that may let us avoid the auxiliary class without zillions of type errors. I don't think it will let us avoid that expected size error on its own. How bad do you think it would be to make the change I suggested removing the If from that check?

TBH I don't know. What he proposes sounds like something that will require a lot of effort and most likely it's not worth it.

For one thing because, as I mentioned before, dipT is considered experimental and I doubt anyone is using it, although that's no good reason on its own.

More importantly, I suspected that with some (likely more) effort, constraints like ConstraintDIPNLorentz could be revisited (as you pointed out yourself IIRC), which might be beneficial for this issue but not just that. As you can see from its comment:

-- The first constraint here is sufficient to make 'dipN' compile.
-- However, it is not enough for good type inference. If we use only the first
-- constraint, '_example' below will not compile because GHC will not be able
-- to deduce type of the input stack for 'unit'.

these are heavily based on what GHC can and cannot do which seems to have changed quite a bit in GHC 9.

Lastly, IMO if we need to spend much more time on this typeclass approach it would be better to use your other MR, even tho we both would have preferred a different solution.

If you agree I would proceed this way:

use the simplest typeclass-based approach in this MR despite the repeating error.
open another issue to revisit and simplify "composite constraints" on instructions in morley and lorentz
open yet another issue to solve the repeating error caused by this MR, but that should wait for (2) to be solved as it's possibly a solution

I think I understand what you're saying.... By "repeating error" I'm guessing you mean the extra error about list length? Because if you mean the one with zillions of duplicates I can't make sense of the rest of the plan. I do think we can probably make some good progress by the plan as I understand it.

By "repeating error" I'm guessing you mean the extra error about list length?

No, I meant the one with several duplicates

This error we actually want (it happens too many time, but it should happen) as it's the one that pops out when a stack without an element of the needed type is given to an use of dipT.

The extra error about the list length happens on the definition of dipT itself for me and it's not really an extra, as we'd want it to not happen at all

I didn't find a way to avoid it (or rather to convince GHC that such length constraint is in fact satisfied), but if you do can find a way to do so it would be great, it may even solve the issue with the first repeated error.

I'll need to make sure we don't also get the extra error along with the duplicates. And I'll think a bit about whether there's a clean way to avoid the silly extras.

I don't see the extra error along with all the repetitions, but I also don't see any reason why I don't. I would personally feel a lot more comfortable about this whole thing if we changed the definition of RequireLongerOrSameLength' so it will only produce an error when there's a definite length mismatch. That does change error messages in ambiguous type situations, but honestly I'm not confident we can reliably do a good job there anyway (see #561 (comment 1059299533) for a particularly scary example). I've come up with another option to play around with, based on Adam Gundry's suggestion. It seems to avoid the problems we've been having.

instance ( dipInp ~ (a ': tail_dipInp)
         , RequireNonEmpty
             ('Text "dipT requires a Lorentz instruction that takes input on the stack.")
             dipInp
         , TheOnlyC (StackElemNotFound inp a)
                    (StackElemAmbiguous inp a)
                    (LS.FindIndices (DefaultEqSym1 a) inp)
                    indexGHC
         , index ~ ToPeano indexGHC
         , ConstraintDIPNLorentz index inp out dipInp dipOut
         ) =>
  DipT a inp dipInp dipOut out where
  dipT = dipNPeano @index

-- | A class form of TheOnly. I couldn't see a way to get the fundeps we
-- want with a constraint family.
class TheOnlyC (empty_err :: ErrorMessage) (many_err :: ErrorMessage) (xs :: [k]) (x :: k)
  | xs -> x
instance (TypeError e_err, Determined y) => TheOnlyC e_err m_err '[] y
instance x ~ y => TheOnlyC e_err m_err '[x] y
instance (TypeError m_err, Determined y) => TheOnlyC e_err m_err (x1 ': x2 ': xs) y

-- | This can be used to satisfy a fundep in an instance constraint
-- for an error instance.
class Determined (x :: k) | -> x

-- | This should be added to whichever option we choose; the error
-- messages GHC generates by itself are not very nice in context.
type family RequireNonEmpty (e :: ErrorMessage) (xs :: [k]) :: Constraint where
  RequireNonEmpty e '[] = TypeError e
  RequireNonEmpty _ _ = ()

Looking more broadly, I think these sorts of changes should work pretty well when an internal family can't error out when things are okay up above. However, something more/different will likely be needed in other cases.

I've come up with another option to play around with, based on Adam Gundry's suggestion. It seems to avoid the problems we've been having.

I see, it doesn't seem terribly ad-hoc to me and hopefully I'm not wrong (as it may be useful elsewhere).

If that indeed solves our problem let's update this MR and use it here

I would personally feel a lot more comfortable about this whole thing if we changed the definition of RequireLongerOrSameLength' so it will only produce an error when there's a definite length mismatch.

I agree, that would likely be an improvement, all things considered.

So let's slightly change the plan above to:

use this new solution of yours here
open a separate issue to change RequireLongerOrSameLength', and similar, to change their behavior in ambiguous situations
open another issue to revisit and simplify "composite constraints" on instructions, like ConstraintDIPNLorentz, which will be affected by the previous one

How does that sound?

Sounds good to me!

OK, I've updated the MR. I took the liberty of expanding out to include dupT as well as dipT, because it's a trivial reuse of the same machinery.

added 1 commit

a0fe6d58 - [#6 (closed)] Implement dipT using dipN

Compare with previous version

added 1 commit

e0f4ba1b - [#6 (closed)] Implement dipT using dipN

Compare with previous version

added 1 commit

b523be88 - fixup

Compare with previous version

requested review from @pasqu4le and @lierdakil

@pasqu4le would you like me to take a few minutes today to try to reduce this so I can test against the latest GHC and file a bug report if appropriate?

@david.feuer yes, please do.

I think that regardless of our issue it would be great to report it, if it's indeed a GHC issue.

I've reported it as GHC issue #22126.

Ok, I see, hopefully this will be solved there.

It will be a while before this can be used by us however (as we'll have to wait that it's in a stack LTS after it is solved), so in the meanwhile we have to deal with it.

TBH I'm kind willing to accept it and go with a solution like the first one mentioned èabove+(!1198 (comment 1079379200)).

I mean, it's annoying, but I don't think that it's very confusing: one can easily see that the message is the same one IMO.

What do you think? AFAIK our option are either this or to fall back to the approach in your previous MR, !1197 (closed)

marked this merge request as ready

added 1 commit

ac0afd29 - [#6 (closed)] Implement dipT using dipN

Compare with previous version

added 1 commit

62135161 - [#6 (closed)] Implement dipT using dipN and dupT using dupN

Compare with previous version

changed title from [#6 (closed)] Implement dipT using dipN to [#6 (closed)] Implement dipT using dipN and dupT using dupN

changed the description

added 1 commit

2292b03f - [#6 (closed)] Implement dipT using dipN and dupT using dupN

Compare with previous version

added 1 commit

91590b0c - [#6 (closed)] Implement dipT using dipN and dupT using dupN

Compare with previous version

Okay, I didn't quite grok what's going on here entirely, but the question I have is does this need to be a type class?

Even if we're going for "type class synonym" approach (which I don't know if it's actually required here), dupT could just as well be a simple function and not a class "method", no?

What do you suggest exactly?

Something like this, probably:

dupT :: forall a st indexGHC succ_index.
        ( st ~ (LS.Head st ': LS.Tail st)
         , TheOnlyC (StackElemNotFound st a)
                    (StackElemAmbiguous st a)
                    (LS.FindIndices (DefaultEqSym1 a) st)
                    indexGHC
         , succ_index ~ 'Peano.S (ToPeano indexGHC)
         , ConstraintDUPNLorentz succ_index st (a ': st) a
         , Dupable a
         ) => st :-> a : st
dupT = dupNPeano @succ_index

AFAICT this is exactly equivalent except without type class (one caveat, GHC complains TheOnlyC is redundant when it in fact isn't, but that's easy enough to silence either with the Dict trick or with OPTIONS_GHC).

What I'm trying to get at, why do we introduce a type class here to begin with? Is there any benefit to having it?

The same goes for dipT, albeit it's a wee bit more complex with fundeps (but those can be emulated with equality constraints I think?)

What you're proposing seems more complicated, and exposes more internal machinery in Haddocks, What harm is there in having the class?

seems more complicated

It's just constraints on the instance combined with class constraints, how is this more complicated? It's literally the same code

exposes more internal machinery in Haddocks

Those are exposed anyway, albeit in a less obvious place (i.e. in the instance head).

What harm is there in having the class?

And I ask again what benefit is there to having a class? To be clear, I'm not yet arguing for or against, I'm trying to understand the rationale for why it's there. With dipT I can kinda see the reasoning (that being fundeps are arguably simpler than explicitly writing out equality constraints), here, with dupT, I don't really see any benefit to having a type class. I might be missing something.

@lierdakil, I finally looked into your way a little more closely. For what we currently export, it might work okay (though I haven't played around to see what its error messages look like when things go wrong). But having the class is very helpful for writing polymorphic things based on it (as we currently define dropT in terms of dipT). We could use a constraint synonym to remove duplication, but we'd still need to mention (and hide, with explicitly inferred type arguments) the index. Unless we calculate the index twice, once in a way that gives an error message and once in a way that produces a stuck type. I guess we could, but what's the point?

Perhaps you could hide the index with quantified constraints (didn't really think this through, so maybe not). At that point however it's not any simpler than the current implementation, so that's beside the point.

I didn't really consider the use case of polymorphic code, I agree that a type class is likely more useful than a constraint synonym in that context.

Could you perhaps add a _dupSample3 with polymorphism, so it's a little more obvious how DupT is intended to be used?

We already use it for dropT.

added 1 commit

35bc728f - A little more inference

Compare with previous version

 ----------------------------------------------------------------------------
 -- | Allows duplicating stack elements referring them by type.
 class DupT (origSt :: [Type]) (a :: Type) (st :: [Type]) where
   dupTImpl :: st :-> a : st
 instance TypeError (StackElemNotFound origSt a) =>
          DupT origSt a '[] where
   dupTImpl = error "impossible"
 instance {-# OVERLAPPING #-}
          ( If (a `IsElem` st)
             (TypeError (StackElemAmbiguous origSt a))
             (() :: Constraint)
 class st ~ (LS.Head st ': LS.Tail st) => DupT (a :: Type) (st :: [Type]) where

[#6] Implement dipT using dipN and dupT using dupN

Description

Related issue(s)

Checklist for your Merge Request

Related changes (conditional)

Stylistic guide (mandatory)

Merged by David Feuer 2 years ago (Sep 22, 2022 7:35pm UTC) 2 years ago

Activity

[#6] Implement dipT using dipN and dupT using dupN

Description

Related issue(s)

Checklist for your Merge Request

Related changes (conditional)

Stylistic guide (mandatory)

Merge request reports

Merged by David Feuer 2 years ago (Sep 22, 2022 7:35pm UTC) 2 years ago

Activity