Detect type equiv for System.Tuple`8

[gusty]

This will allow the constraint solver to detect type equivalences between compiled and syntactic tuples over 8 elements.

[NinoFloris]

Welcome fix! Running into this as well @cartermp

[cartermp]

Looks like this addresses #9639 ? @gusty do you still intend on this being a draft?

[NinoFloris]

Will this also compile for:

     let areEqualT9 = System.Tuple<_,_,_,_,_,_,_,(int * int)>(1,2,3,4,5,6,7,(8,9)) = (1,2,3,4,5,6,7,8,9) 

[gusty]

I just added a commit that will allow that.

[gusty]

@cartermp I did this as part of #9605 but realized that it’s really a fix of an inconsistent behavior of the compiler, so I wouldn’t be surprised that someone else encountered this issue.

It’s in draft because I’m not 100% sure it’s complete. There might be more cases I’m missing.

I’ll have another look later and let you know.

[NinoFloris]

About c61e3ad, unless I read it wrong I think we should strongly normalize System.Tuple to syntactic tuples but not vice versa. Allowing tuples at 8th position in syntactic tuples to stand in for TRest does not sound right. In such cases TRest should be Tuple<(int * int)> not Tuple<int, int>.

[gusty]

I wish we could convert all inferred tuples to syntactic tuples but that's not possible or it's too complicated.

So, our best alternative is enforcing type equivalence, which is what this PR does, now syntactic tuples and system tuples could appear at any side of the equality.

Your code, won't compile if we don't have the other way around.

Again, if we're talking about normalizing I agree with you, but that's not what this PR does.

[TIHan]

When we type-check an application, System.Tuple gets decompiled into TType_tuple.

    // Try to decode System.Tuple --> F~ tuple types etc.
    let ty = g.decompileType tcref actualArgTys

Are we not able to do the same here? This is how we started trying to normalize tuples.

[dsyme]

When we type-check an application, System.Tuple gets decompiled into TType_tuple.

Are we not able to do the same here? This is how we started trying to normalize tuples.

This was my first thought as well - why are we not normalizing here?

However I know the reason - we normlize as types to TType_tuple as they are read from .NET metadata, but not if you construct and use these types explicitly in F#. So basically, the design at the moment is simply not to write or use the tuple type encodings explicitly in F#. I believe this is called out in the F# language spec.

Which makes me wonder, what are people doing writing the encoded types? This just isn't supported

I suspect these is really no coherent design in F# that supports using these types directly, because the encoding can be "revealed" by generic instantiation - indeed #9639 deals with one example of this. Here's another:

    let f x = System.Tuple<_,_,_,_,_,_,_,_>(1,2,3,4,5,6,7,x  ) // result of 'f' is not a valid encoded tuple - yet

    f (System.Tuple<_> (8)) // result of 'f' is now a valid encoded tuple

This kind of situation makes me very reluctant to do an adhoc job of making these tuple encodings usable directly in the F# programming model. I simply don't know the impact of teaching the unification algorithm and other type relations about these equations. Things can get very very subtle when extra equations are thrown in adhoc. It might be that the change here is the correct way to teach the sytem about these, but there would have to be 1000s of lines of quite subtle tests to prove this to me.

So, in brief, #9639 is by design and you just shouldn't be writing and using encoded tuple types directly in F#. Let the compiler do the job.

[NinoFloris]

@dsyme #9605 IMHO is more interesting.

If you're saying we shouldn't implement any fix here then I see no generic way to deal with syntactic tuples, wouldn't opting into using the encoding be enough of a signal you're coupling yourself to .NET?

The issue I have today is that there's no way to force an unknown shaped Tuple<...TRest> back into a syntactical tuple, meaning you end up with a tuple where TRest is actually nested. This PR fixes that but if you have another mechanism in mind I'm sure that would be fine too.

For reference it's horrible code like this

    type TupleApp =
        static member inline Invoke arg (t: 'tuple) =
            let inline call (a: ^a, f, b: ^b) = ((^a or ^b) : (static member App: _*_*_ -> _) b, f, a)
            call (Unchecked.defaultof<TupleApp>, arg, t)

        static member inline App (t: 't, arg, _: TupleApp) =
            let t1, t2, t3, t4, t5, t6, t7, tr =
                (^t : (member Item1 : ('a -> _)) t),
                (^t : (member Item2 : ('a -> _)) t),
                (^t : (member Item3 : ('a -> _)) t),
                (^t : (member Item4 : ('a -> _)) t),
                (^t : (member Item5 : ('a -> _)) t),
                (^t : (member Item6 : ('a -> _)) t),
                (^t : (member Item7 : ('a -> _)) t),
                (^t : (member Rest  : _) t)

            Tuple<_,_,_,_,_,_,_,_> ((t1 arg), (t2 arg), (t3 arg), (t4 arg), (t5 arg), (t6 arg), (t7 arg), (TupleApp.Invoke arg tr))

        static member inline App (x: Tuple<_>                 , arg, _: TupleApp) = Tuple<_> (x.Item1 arg)
        static member inline App ((t1, t2)                    , arg, _: TupleApp) = Tuple<_,_> ((t1 arg), (t2 arg))
        static member inline App ((t1, t2, t3)                , arg, _: TupleApp) = Tuple<_,_,_> ((t1 arg), (t2 arg), (t3 arg))
        static member inline App ((t1, t2, t3, t4)            , arg, _: TupleApp) = Tuple<_,_,_,_> ((t1 arg), (t2 arg), (t3 arg), (t4 arg))
        static member inline App ((t1, t2, t3, t4, t5)        , arg, _: TupleApp) = Tuple<_,_,_,_,_> ((t1 arg), (t2 arg), (t3 arg), (t4 arg), (t5 arg))
        static member inline App ((t1, t2, t3, t4, t5, t6)    , arg, _: TupleApp) = Tuple<_,_,_,_,_,_> ((t1 arg), (t2 arg), (t3 arg), (t4 arg), (t5 arg), (t6 arg))
        static member inline App ((t1, t2, t3, t4, t5, t6, t7), arg, _: TupleApp) = Tuple<_,_,_,_,_,_,_> ((t1 arg), (t2 arg), (t3 arg), (t4 arg), (t5 arg), (t6 arg), (t7 arg))

    let f x = x
    let tup9 = (f, f, f, f, f, f, f, f, f)
    
    // inferred unit -> Tuple<int,int,int,int,int,int,int,(int * int)>
    let test() = TupleApp.Invoke 1 tup9

    // Error: This expression was expected to have type ''a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i' but here has type 'Tuple<int,int,int,int,int,int,int,(int * int)>'
    let (one, two, three, four, five, six, seven, eight, nine) = test()

A much simpler case is this

    let x = System.Tuple<int,int,int,int,int,int,int,_>(1,2,3,4,5,6,7,System.Tuple<int, int>(8,9))
    // Error: This expression was expected to have type ''a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i' but here has type 'Tuple<int,int,int,int,int,int,int,(int * int)>'
    let (one, two, three, four, five, six, seven, eight, nine) = x

    // Though here you could maybe fix things by casting like so; this is impossible to do generically.
    let (one, two, three, four, five, six, seven, eight, nine) = unbox<int * int * int * int * int * int * int * int * int> x

How do you deal with .NET tuple types such that they can be patterned matched without nesting past 7 args?
I would love for the compiler to just do the job, in fact that's really all I'm asking for.

[dsyme]

If you're saying we shouldn't implement any fix here then I see no generic way to deal with syntactic tuples, wouldn't opting into using the encoding be enough of a signal you're coupling yourself to .NET?

That's right, in the current design of F# there is no intention to give a statically-resolved way to write generic inlined SRTP code that works over any tuple type. That is, there's no intention to support writing generic SRTP code w.r.t. the encoding of tuples.

I get what you're trying to do and why it seems "oh so close" to working. However it was never intended to work. If we did support this I think it would ideally be an extension to SRTP constraints with respect to the F# source tuple types, not the encoding. But SRTP just wasn't designed to support this kind of generic programming.

[NinoFloris]

I expected as much, and I'm 'ok' with what it's doing right now.

For the curious readers thinking "why would you ever write or need this"; this code is used for an inference driven reader CE. A custom operation on the builder enables you to request common dependencies outside function arguments. It's really quite a joy to use.

// inferred type ContextTask<'a, Widget voption> when 'a :> DbConnection and 'a :> Logging and 'a :> Tenant
let findWidget widgetId = contextTask {
    arguments (Service.dbConnection, Service.logging, Service.tenant) into (dbConn, logger, tenant)
    try 
        return! dbConn.TrySingle<Widget>("SELECT * FROM widgets WHERE id = @widgetId AND tenantId = @tenantId", {| widgetId = widgetId; tenantId = tenant.Id |})
    with ex -> 
        return logger.LogError("Oh no", ex)
} 

To do that arguments must be polyvariadic (infinite differently typed args) to allow for the separate return types of the dependencies, and as a result TupleApp was born.
For completeness sake I had hoped to have it function identically for all argument lengths but I can live with the 7 arguments 'until it gets unpleasant' limit, more should be viewed as a code smell anyway.

[dsyme]

I expected as much, and I'm 'ok' with what it's doing right now.

OK cool. I will close this then, thank you for the example too

[NinoFloris]

If we did support this I think it would ideally be an extension to SRTP constraints with respect to the F# source tuple types, not the encoding

Hypothetically what would this look like? I expect some primitive type level pattern matching would be necessary.
However how to inductively construct (and with minimal additional syntax express) a flat n-tuple is something I'm still not clear on. This gap in particular is the crux of why we're abusing the underlying encoding.

[gusty]

I think we all agree that the sole action of declaring this behavior as by-design doesn't automatically make it more consistent.

I was thinking, in order to solve this inconsistency at some point sooner or later we'll need to add a new static constraint that indicates that a type is a tuple of a yet unknown arity.

So if we take @dsyme example, typed inline, it would give:

let inline f x = System.Tuple<_,_,_,_,_,_,_,_>(1,2,3,4,5,6,7,x) 
// val inline f : x:'a -> System.Tuple<int,int,int,int,int,int,int,'a when 'a : tuple>

then there's no possibility of creating an invalid tuple, and at the same time we can, at the very last step of type inference, convert all tuples of known arity to a syntactic one. This way, when calling the above function, we'll get:

> f (System.Tuple<_> (8)) ;;
val it : int * int* int* int* int* int* int* int =
  (1, 2, 3, 4, 5, 6, 7, 8)

instead of val it : System.Tuple<int,int,int,int,int,int,int,System.Tuple<int>>

So, supplying a generic parameter won't resolve the constraint and convert to syntactic, but if we supply a tuple, even if it's generic but its arity is know, like 'a * 'b it resolves, unless of course it's another 8-non-encoded tuple.

Another constraint should be added for struct tuples: ^T when ^T : struct tuple.