Program that should not compile, using statically resolved type parameters, gets runtime exception instead #4924
Comments
|
If it is useful, I now have a branch where I got the compile to fail by using more member constraints to fake out type-level guarantees on the conceptual higher-kinded types I was trying to model. This is a verbose workaround but one that bolsters the overall solidity of my code and in my mind the fact that it worked probably does reduce the severity of this bug. |
|
I'm seriously impressed by this code, I've never used SRTP to such complexity. I'm curious, as I see quite some syntax that doesn't compile with F# 4.0, and I wasn't aware of syntax changes or significant added features in F# 4.1. Which makes you wonder whether this is caused by the new feature's implementation or that this has always been a bug (provided it is one, I cannot be the judge of that). Not sure if this can be rewritten with F# 4.0 syntax though and if so, whether that would yield the same results. I've managed before to create compilable code with SRTP, that threw hard-to-diagnose errors. In my case that was caused by the compiler allowing the order to be random on static inline class members, but that in reality they need to be in the correct order, as if they are in a module, otherwise inexplicable compile or runtime errors can occur. Since you use a lot of static members, I would wonder whether this could in any way be related to an issue with the order of declaration. Just my 2p, perhaps not very useful, but your code intrigued me ;). PS: it may be useful to add what would be the correct way of calling your code, to see it run without that error. You write "This type clearly does not match the implementation", and I'm sure for some people it is "clear", but it wasn't for me, and I find SRTP quite hard to read and diagnose whenever it gets beyond a few lines. |
|
@abelbraaksma Thanks for your intriguing comments. I will certainly own up to the fact that this is insanely complex SRTP code. Polite of you to say you are impressed; you should rather say disgusted! But sadly, it's the part of my codebase keeping me sane (there is much much more code written in this style in my actual code base: I'm a bit of a crackpot I suppose). Basically I have found that if you write code with Yes, this code is enabled by F# 4.1 and was not possible in F# 4.0 AFAIK. I looked into it in F# 4.0 and couldn't see a way to make it work anyhow. My coworker resurrected the question after they added the new tweaks in F# 4.1 and as odd as the little addition was it allowed us to make it all work (or so we thought, haha!). Good thought about ordering. I don't pretend to understand what's happening well enough to know whether that is the issue at stake but it's good to know that someone else has hit something like this. You are right in saying I was a bit hasty about saying it was "clear" that the type didn't match the implementation; should have explained a bit. The intend of with the specific conditions that both I recognize that in some sense I am abusing F# in all this. Perhaps the users who abuse the program are the ones who tend to find the bugs. |
|
Hi @Kazark, I'm hesitant to say that your example is written incorrectly, because nobody's ever issued a guide on the "correct" way to write SRTP, but congratulations (?) on your journey along the unmarked path to, uh, SRTP enlightenment, or something. You're correct that some of the constructs you're using weren't possible until F# 4.1; in fact, I'm guilty of having made it easier when I reported one of the things you're now using in #392 (wow, that was a long time ago). The reason you're getting the let inline f (x : ^a) = (^a : (member ToString : unit -> string) x)
// which is
val inline f : x: ^a -> string when ^a : (member ToString : ^a -> string)
let () = printfn "%s" (f 1)
(*
System.NullReferenceException: Object reference not set to an instance of an object.
at <StartupCode$FSI_0003>.$FSI_0003.main@()
Stopped due to error
*)Yet, this works fine: let inline f x = (^a : (member ToString : unit -> string) (x :> obj))
(* harmless warning about ^a being solved to obj *)
val inline f : x:'a -> string...and of course, constraints not involving bowels of .NET tend to be far better behaved already: let inline g x = (^a : (member Hoopty : unit -> string) x)
// which is
val inline g : x : ^a -> string when ^a : (member Hoopty : ^a -> string)
let _ = g 1
(*
g 1;;
--^
stdin(16,4): error FS0001: The type 'int' does not support the operator 'Hoopty'
*)But I digress. Indeed, SRTP "abuse" such as this is a part of the language few users explore, and despite its utility (nobody is arguing that it does not enable a number of things otherwise not possible) there does seem to be some sentiment that its use is a bridge too far. That said, the code you've written goes against one of the (unwritten) teachings of the SRTP Elders: instead of using explicit type parameters in order to add to solver's overload candidate set, you need to instead--unfortunately--pass a dummy value (i.e. term, not type) that will appropriately influence the solver. I'm sure you've probably noticed that most ways of trying to avoid the dummy value result in strange errors from the compiler involving internally-generated type parameters with names like So, let's apply this one weird trick discovered by a local F# wonk (compiler authors hate him!): diff --git a/SRTP/SRTP.fs b/SRTP/SRTP.fs
index d23fd18..8b6a499 100644
--- a/SRTP/SRTP.fs
+++ b/SRTP/SRTP.fs
@@ -28,37 +28,41 @@ type Multifunctor() =
static member inline mapB (f : ^b -> ^b0, x : Either< ^a,^b>) : Either< ^a,^b0> = Either.rmap f x
static member inline mapB (f : ^b -> ^b0, (a : ^a, b : ^b, c : ^c)) : ^a * ^b0 * ^c = (a, f b, c)
-let inline mapB_< ^mf, ^f, ^a, ^b when (^mf or ^a) : (static member mapB : ^f * ^a -> ^b)> (f : ^f, x : ^a) : ^b =
- ((^mf or ^a) : (static member mapB : ^f * ^a -> ^b) (f, x))
+ static member inline Invoke (f : ^f, x : ^a) =
+ let inline call (d : ^mf) =
+ ((^mf or ^b) : (static member mapB : ^f * ^a -> ^b) (f, x)) in
+ call Unchecked.defaultof<Multifunctor>
+
+let inline mapB_ (f : ^f, x : ^a) : ^b = Multifunctor.Invoke (f, x)
let inline mapB (f : ^f) (x : ^a) : ^b when (Multifunctor or ^a) : (static member mapB : ^f * ^a -> ^b) =
- mapB_<Multifunctor,^f,^a,^b> (f, x)
+ mapB_ (f, x)
type Multiapplicative() =
static member inline wrapB (_ : Either< ^a,^b>, x0 : ^b) : Either< ^a,^b> = Right x0
static member inline wrapB (_ : Result< ^a,^b>, x0 : ^b) : Result< ^a,^b> = Error x0
-let inline wrapB_< ^mf, ^a, ^b when (^mf or ^b) : (static member wrapB : ^b * ^a -> ^b)> (instance : ^b, x : ^a) : ^b =
+let inline wrapB_ (instance : ^b, x : ^a) : ^b =
((^mf or ^b) : (static member wrapB : ^b * ^a -> ^b) (instance, x))
let inline wrapB (x : ^a) : ^b when (Multiapplicative or ^b) : (static member wrapB : ^b * ^a -> ^b) =
- wrapB_<Multiapplicative,^a,^b> (Unchecked.defaultof< ^b>, x)
+ wrapB_ (Unchecked.defaultof< ^b>, x)
type Multimonad() =
static member inline bindB (f : ^b -> Either< ^a,^b0>, x : Either< ^a,^b>) : Either< ^a,^b0> = Either.rbind f x
static member inline bindB (f : ^b -> Result< ^a,^b0>, x : Result< ^a,^b>) : Result< ^a,^b0> = failwith "TODO: why u no haz Result.errorBind"
-let inline bindB_< ^mf, ^f, ^a, ^b when (^mf or ^a) : (static member bindB : ^f * ^a -> ^b)> (f : ^f, x : ^a) : ^b =
+let inline bindB_ (f : ^f, x : ^a) : ^b =
((^mf or ^a) : (static member bindB : ^f * ^a -> ^b) (f, x))
let inline bindB (f : ^f) (x : ^a) : ^b when (Multimonad or ^a) : (static member bindB : ^f * ^a -> ^b) =
- bindB_<Multimonad,^f,^a,^b> (f, x)
+ bindB_ (f, x)
type Multitraverse() =
static member inline traverseBB (f : ^b -> ^b0, (a : ^a, b : ^b)) : ^b1
when (Multifunctor or ^b0) : (static member mapB : _ * ^b0 -> ^b1) =
- mapB_<Multifunctor,_,_,_> (addfst a, (f b))
+ mapB_ (addfst a, (f b))
static member inline traverseBB (f : ^a -> ^a0, (_ : ^b, b : ^a, _ : ^c) as t) : ^a1
when (Multifunctor or ^a0) : (static member mapB : _ * ^a0 -> ^a1) =
- mapB_<Multifunctor,_,_,_> ((fun x -> mapB (k x) t), f b)
+ mapB_ ((fun x -> mapB (k x) t), f b)
static member inline traverseBB (f : ^b -> ^b0, x : Either< ^a,^b>) : ^b1
when (^b0 or Multiapplicative) : (static member wrapB : _ -> ^b0)
@@ -67,12 +71,12 @@ type Multitraverse() =
and (^b1 or Multifunctor) : (static member mapB : _*_ -> _ ) =
Either.match_ (Left >> wrapB) (mapB Right << f) x
-let inline traverseBB_< ^mf, ^a, ^b, ^c, ^d when (^mf or ^a) : (static member traverseBB : (^a -> ^b) * ^c -> ^d)> (f : ^a -> ^b, x : ^c) : ^d =
+let inline traverseBB_ (f : ^a -> ^b, x : ^c) : ^d =
((^mf or ^a) : (static member traverseBB : (^a -> ^b) * ^c -> ^d) (f, x))
let inline traverseBB (f : ^a -> ^b) (x : ^c) : ^d
when (Multitraverse or ^c) : (static member traverseBB : (^a -> ^b) * ^c -> ^d)
and (Multimonad or ^b) : (static member bindB : (_ -> ^b) * ^b -> ^b) =
// The intent of requiring monad is just trying to be lawful
- traverseBB_<Multitraverse,^a,^b,^c,^d> (f, x)
+ traverseBB_ (f, x)Now our program fails to typecheck as hoped: Hope this helps in the meantime. I've submitted a talk to Open F# this year about this very kind of thing, so if it gets in then it should be right up your alley! Also, I suspect you'll find FSharpPlus to be a very useful library in this same vein. @cartermp I'll let you know where to send the coffee. ;) |
|
@drvink Wow, thanks for the detailed response. I may respond more after digesting it. |
|
@drvink Thanks for your guidance on SRTP. I will update my code accordingly. Indeed, it is not well documented; haha! I actually fixed an error in the docs while trying to learn about it, lol... |
|
@Kazark no problem--and yes, more documentation would be great! |
|
@Kazark We will need a much smaller minimal repro of the underlying problem - that's a whole lot of SRTP in that repro. It's a good stress test I suppose, but it's not the kind of use of SRTP I'd personally want to encounter often :) |
dsyme
added
Bug
Area-Compiler
Impact-Medium
|
OK I need to update my example further. Appears for me only in the example repository. |
|
So one thing to note here is that replacing (^mf or ^a) with (^mf or ^b) as support at https://github.com/Kazark/fsharp-srtp-broken/blob/master/SRTP/SRTP.fs#L32 reports back the expected type error. |
|
The extracted code with changed variable names fails at the stage of the code generation too just like #5973. type Bar =
static member inline bar (f : ^b -> ^b0, (a : ^a, b : ^b)) : ^a * ^b0 = (a, f b)
static member inline bar (f : ^b -> ^b0, (a : ^a, b : ^b, c : ^c)) : ^a * ^b0 * ^c = (a, f b, c)
let inline bar_< ^bar, ^f, ^a, ^b when (^bar or ^b) : (static member bar : ^f * ^a -> ^b)> (f : ^f, x : ^a) : ^b =
((^bar or ^b) : (static member bar : ^f * ^a -> ^b) (f, x))
type Foo =
static member inline foo (f : ^b -> ^b0, (a : ^a , b : ^b)) : ^b1
when (Bar or ^b1) : (static member bar : _ * ^b0 -> ^b1) =
bar_<Bar,_,_,_>( a |> (fun x y -> (x, y)), (f b))
static member inline foo (f : ^a -> ^b, (a, b, c)) : ^c =
Unchecked.defaultof< ^c>
let inline foo_< ^foo, ^a, ^b, ^c, ^d when (^foo or ^a) : (static member foo : (^a -> ^b) * ^c -> ^d)> (f: ^a -> ^b) (x: ^c) : ^d =
((^foo or ^a) : (static member foo : (^a -> ^b) * ^c -> ^d)(f, x))
let inline foo (f: ^a -> ^b) (x: ^c) : ^d when (Foo or ^a) : (static member foo: (^a -> ^b) * ^c -> ^d)=
foo_<Foo, ^a, ^b, ^c, ^d> f x
let test = (fun (a:int) -> float a)
let partialAppliedFoo : (int * int) -> float * int =
foo testMoreover it's possible to write whatever return type you like at the end, the compiler will tell the Due to excessive testing I believe this might be an issue related to using member functions which are inline. The Constraints are not propagated correctly. Also a possible reason for failures could be that constraints aren't coupled to a method anymore as soon as the support of the constraint contains only concrete types (which still may be linked to a parameter but not taken into account for type inference). With that idea the example could also be seen as super rare edge case. |
|
My code above is a different issue, however I extracted an example of the example which is smaller. type Either<'l,'r> = Left of 'l | Right of 'r
type Maybe<'a> = Either<unit,'a>
let k x _ = x
let inline flip f x y = f y x
let inline addfst x y = (x, y)
module Either =
let match_ fl fr : Either<'l,'r> -> 'a =
function Right x -> fr x | Left x -> fl x
let rmap f : Either<'l,'a> -> Either<'l,'b> =
function Right x -> Right (f x) | Left e -> Left e
let rbind f : Either<'l,'a> -> Either<'l,'b> =
function Right x -> f x | Left e -> Left e
type Multifunctor() =
static member inline mapB (f : ^b -> ^b0, (a : ^a, b : ^b)) : ^a * ^b0 = (a, f b)
static member inline mapB (f : ^b -> ^b0, x : Either< ^a,^b>) : Either< ^a,^b0> = Either.rmap f x
static member inline mapB (f : ^b -> ^b0, (a : ^a, b : ^b, c : ^c)) : ^a * ^b0 * ^c = (a, f b, c)
let inline mapB_< ^mf, ^f, ^a, ^b when (^mf or ^a) : (static member mapB : ^f * ^a -> ^b)> (f : ^f, x : ^a) : ^b =
((^mf or ^a) : (static member mapB : ^f * ^a -> ^b) (f, x))
let inline mapB (f : ^f) (x : ^a) : ^b when (Multifunctor or ^a) : (static member mapB : ^f * ^a -> ^b) =
mapB_<Multifunctor,^f,^a,^b> (f, x)
type Multiapplicative() =
static member inline wrapB (_ : Either< ^a,^b>, x0 : ^b) : Either< ^a,^b> = Right x0
static member inline wrapB (_ : Result< ^a,^b>, x0 : ^b) : Result< ^a,^b> = Error x0
let inline wrapB_< ^mf, ^a, ^b when (^mf or ^b) : (static member wrapB : ^b * ^a -> ^b)> (instance : ^b, x : ^a) : ^b =
((^mf or ^b) : (static member wrapB : ^b * ^a -> ^b) (instance, x))
let inline wrapB (x : ^a) : ^b when (Multiapplicative or ^b) : (static member wrapB : ^b * ^a -> ^b) =
wrapB_<Multiapplicative,^a,^b> (Unchecked.defaultof< ^b>, x)
type Multitraverse() =
static member inline traverseBB (f : ^b -> ^b0, (a : ^a, b : ^b)) : ^b1
when (Multifunctor or ^b0) : (static member mapB : _ * ^b0 -> ^b1) =
mapB_<Multifunctor,_,_,_> (addfst a, (f b))
static member inline traverseBB (f : ^b -> ^b0, x : Either< ^a,^b>) : ^b1
when (^b0 or Multiapplicative) : (static member wrapB : _ -> ^b0)
and (^b0 or Multifunctor) : (static member mapB : _*_ -> _ )
and (^b1 or Multiapplicative) : (static member wrapB : _ -> ^b1)
and (^b1 or Multifunctor) : (static member mapB : _*_ -> _ ) =
Either.match_ (Left >> wrapB) (mapB Right << f) x
let inline traverseBB_< ^mf, ^a, ^b, ^c, ^d when (^mf or ^a) : (static member traverseBB : (^a -> ^b) * ^c -> ^d)> (f : ^a -> ^b, x : ^c) : ^d =
((^mf or ^a) : (static member traverseBB : (^a -> ^b) * ^c -> ^d) (f, x))
let inline traverseBB (f : ^a -> ^b) (x : ^c) : ^d
when (Multitraverse or ^c) : (static member traverseBB : (^a -> ^b) * ^c -> ^d) =
// The intent of requiring monad is just trying to be lawful
traverseBB_<Multitraverse,^a,^b,^c,^d> (f, x)
let private maybeZero : int -> Maybe<int> =
function
| 0 -> Right 0
| _ -> Left ()
// This type clearly does not match the implementation, and yet it type checks
let private whatInTheWorld : list<string>*int -> Either<string,list<string>> =
traverseBB maybeZeroI've spend many hours on figuring out what goes on there but I'm clueless. |
|
Even smaller repro: type Either<'l,'r> = Left of 'l | Right of 'r
type Maybe<'a> = Either<unit,'a>
let inline addfst x y = (x, y)
module Either =
let rmap f : Either<'l,'a> -> Either<'l,'b> =
function Right x -> Right (f x) | Left e -> Left e
type Multifunctor() =
static member inline mapB (f : ^b -> ^b0, (a : ^a, b : ^b)) : ^a * ^b0 = (a, f b)
static member inline mapB (f : ^b -> ^b0, x : Either< ^a,^b>) : Either< ^a,^b0> = Either.rmap f x
// static member inline mapB (f : ^b -> ^b0, (a : ^a, b : ^b, c : ^c)) : ^a * ^b0 * ^c = (a, f b, c)
let inline mapB_< ^mf, ^f, ^a, ^b when (^mf or ^a) : (static member mapB : ^f * ^a -> ^b)> (f : ^f, x : ^a) : ^b =
((^mf or ^a) : (static member mapB : ^f * ^a -> ^b) (f, x))
type Multitraverse() =
static member inline traverseBB (f : ^b -> ^b0, x : ^a * ^c * ^d) = fun a -> printfn "hi"; a
static member inline traverseBB (f : ^b -> ^b0, (a : ^a, b : ^b)) : ^b1
when (Multifunctor or ^b0) : (static member mapB : (^c -> (^a * ^c)) * ^b0 -> ^b1) =
mapB_<Multifunctor,_,_,_> (addfst a, (f b))
let inline traverseBB_< ^mf, ^a, ^b, ^c, ^d when (^mf or ^a) : (static member traverseBB : (^a -> ^b) * ^c -> ^d)> (f : ^a -> ^b, x : ^c) : ^d =
((^mf or ^a) : (static member traverseBB : (^a -> ^b) * ^c -> ^d) (f, x))
let inline traverseBB (f : ^a -> ^b) (x : ^c) : ^d
when (Multitraverse or ^c) : (static member traverseBB : (^a -> ^b) * ^c -> ^d) =
// The intent of requiring monad is just trying to be lawful
traverseBB_<Multitraverse,^a,^b,^c,^d> (f, x)
let private maybeZero : int -> Maybe<int> =
function
| 0 -> Right 0
| _ -> Left ()
// This type clearly does not match the implementation, and yet it type checks
let private whatInTheWorld : list<string>*int -> Either<unit,list<string> * float> =
traverseBB maybeZero |
|
@realvictorprm, pasting your last code in a console .NET Framework project, and adding a Strangely, I couldn't repro, consecutive runs after restart went fine. I then altered the code to be: which doesn't crash, and shows in the console as:
Not sure if it should crash or work, considering it shouldn't typecheck at all to begin with. |
|
Expected is that it does not compile as it's wrong typed but current behaviour of that snippet is that it compiles fine. You can only "show" that it's wrong if you try to match on the result of the function expecting |
|
Thanks, clearer now (still odd it crashed vs, but perhaps that had an unrelated cause). |
type Foo<'a, 'b> = Bar of 'a * 'b
type Multifunctor() =
static member inline mapB (f : ^b -> ^b0, (a : ^a, b : ^b)) : ^a * ^b0 = (a, f b)
static member inline mapB (f : ^b -> ^b0, x : Foo< ^a, ^b>) = f
let inline mapB_< ^mf, ^f, ^a, ^b when (^mf or ^a) : (static member mapB : ^f * ^a -> ^b)> (f : ^f, x : ^a) : ^b =
((^mf or ^a) : (static member mapB : ^f * ^a -> ^b) (f, x))
type Multitraverse() =
static member inline traverseBB (f : ^b1 -> ^b2, x : ^a1 * ^c2 * ^d3) = fun a -> printfn "hi"; a
static member inline traverseBB (f : ^b -> ^b0, (a : ^a, b : ^b)) : ^b1
when (Multifunctor or ^b0) : (static member mapB : _ * ^b0 -> ^b1) =
mapB_<Multifunctor,_,_,_> ((fun x -> x), (f b))
let inline traverseBB_< ^mf, ^a, ^b, ^c, ^d when (^mf or ^a) : (static member traverseBB : (^a -> ^b) * ^c -> ^d)> (f : ^a -> ^b, x : ^c) : ^d =
((^mf or ^a) : (static member traverseBB : (^a -> ^b) * ^c -> ^d) (f, x))
let inline traverseBB (f : ^a -> ^b) (x : ^c) : ^d
when (Multitraverse or ^c) : (static member traverseBB : (^a -> ^b) * ^c -> ^d) =
// The intent of requiring monad is just trying to be lawful
traverseBB_<Multitraverse,^a,^b,^c,^d> (f, x)
let private maybeZero : int -> Foo<'a,'b> =
fun x -> Bar(0, 2)
// This type clearly does not match the implementation, and yet it type checks
let private whatInTheWorld : list<string>*int -> System.Random =
traverseBB maybeZerosmaller again. Using DU's with less than 2 generics will result in typecheck errors again. now it's very obvious that the return type is super wrong. |
|
Right now it's so amusing to see what the compiler outputs if at particular points you introduce a new static typvar vs. using existing typvars from parameters 😂 |
|
oh please compare the error output between these 3 codes ahahahaha 😂 It's too funny! type Foo<'a, 'b> = Bar of 'a * 'b
type Multifunctor() =
static member inline mapB (f : ^b -> ^b0, (a : ^a, b : ^b)) : ^a * ^b0 = (a, f b)
static member inline mapB (f : ^b -> ^b0, x : Foo< ^a, ^b0>) = f
let inline mapB_< ^mf, ^f, ^a, ^b when (^mf or ^a) : (static member mapB : ^f * ^a -> ^b)> (f : ^f, x : ^a) : ^b =
((^mf or ^a) : (static member mapB : ^f * ^a -> ^b) (f, x))
type Multitraverse() =
static member inline traverseBB (f : ^b1 -> ^b2, x : ^a1 * ^c2 * ^d3) = fun a -> printfn "hi"; a
static member inline traverseBB (f : ^b -> ^b0, (a : ^a, b : ^b)) : ^b1
when (Multifunctor or ^b0) : (static member mapB : _ * ^b0 -> ^b1) =
mapB_<Multifunctor,_,_,_> ((fun x -> a,x), (f b))
let inline traverseBB_< ^mf, ^a, ^b, ^c, ^d when (^mf or ^a) : (static member traverseBB : (^a -> ^b) * ^c -> ^d)> (f : ^a -> ^b, x : ^c) : ^d =
((^mf or ^a) : (static member traverseBB : (^a -> ^b) * ^c -> ^d) (f, x))
let inline traverseBB (f : ^a -> ^b) (x : ^c) : ^d
when (Multitraverse or ^c) : (static member traverseBB : (^a -> ^b) * ^c -> ^d) =
// The intent of requiring monad is just trying to be lawful
traverseBB_<Multitraverse,^a,^b,^c,^d> (f, x)
let private maybeZero : int -> Foo<int,int> =
fun x -> Bar(0, 2)
// This type clearly does not match the implementation, and yet it type checks
let private whatInTheWorld : list<string>*int -> System.Random =
traverseBB maybeZeroCompiler like => "Ah you want to confuse me? ** you, I give up (Internal error etc...)" Example 2: type Foo<'a, 'b> = Bar of 'a * 'b
type Multifunctor() =
static member inline mapB (f : ^b -> ^b0, (a : ^a, b : ^b)) : ^a * ^b0 = (a, f b)
static member inline mapB (f : ^b -> ^b0, x : Foo< ^a, ^b0>) = f
let inline mapB_< ^mf, ^f, ^a, ^b when (^mf or ^a) : (static member mapB : ^f * ^a -> ^b)> (f : ^f, x : ^a) : ^b =
((^mf or ^a) : (static member mapB : ^f * ^a -> ^b) (f, x))
type Multitraverse() =
static member inline traverseBB (f : ^b1 -> ^b2, x : ^a1 * ^c2 * ^d3) = fun a -> printfn "hi"; a
static member inline traverseBB (f : ^b -> ^b0, (a : ^a, b : ^b)) : ^b1
when (Multifunctor or ^b0) : (static member mapB : _ * ^b0 -> ^b1) =
mapB_<Multifunctor,_,_,_> ((fun x -> a), (f b))
let inline traverseBB_< ^mf, ^a, ^b, ^c, ^d when (^mf or ^a) : (static member traverseBB : (^a -> ^b) * ^c -> ^d)> (f : ^a -> ^b, x : ^c) : ^d =
((^mf or ^a) : (static member traverseBB : (^a -> ^b) * ^c -> ^d) (f, x))
let inline traverseBB (f : ^a -> ^b) (x : ^c) : ^d
when (Multitraverse or ^c) : (static member traverseBB : (^a -> ^b) * ^c -> ^d) =
// The intent of requiring monad is just trying to be lawful
traverseBB_<Multitraverse,^a,^b,^c,^d> (f, x)
let private maybeZero : int -> Foo<int,int> =
fun x -> Bar(0, 2)
// This type clearly does not match the implementation, and yet it type checks
let private whatInTheWorld : list<string>*int -> System.Random =
traverseBB maybeZeroCompiler like => "You poke me again?! I'll give you an overload error although actually the return type is super wrong 😜 Example 3: type Foo<'a, 'b> = Bar of 'a * 'b
type Multifunctor() =
static member inline mapB (f : ^b -> ^b0, (a : ^a, b : ^b)) : ^a * ^b0 = (a, f b)
static member inline mapB (f : ^b -> ^b0, x : Foo< ^a, ^b0>) = f
let inline mapB_< ^mf, ^f, ^a, ^b when (^mf or ^a) : (static member mapB : ^f * ^a -> ^b)> (f : ^f, x : ^a) : ^b =
((^mf or ^a) : (static member mapB : ^f * ^a -> ^b) (f, x))
type Multitraverse() =
static member inline traverseBB (f : ^b1 -> ^b2, x : ^a1 * ^c2 * ^d3) = fun a -> printfn "hi"; a
static member inline traverseBB (f : ^b -> ^b0, (a : ^a, b : ^b)) : ^b1
when (Multifunctor or ^b0) : (static member mapB : _ * ^b0 -> ^b1) =
mapB_<Multifunctor,_,_,_> ((fun x -> x), (f b))
let inline traverseBB_< ^mf, ^a, ^b, ^c, ^d when (^mf or ^a) : (static member traverseBB : (^a -> ^b) * ^c -> ^d)> (f : ^a -> ^b, x : ^c) : ^d =
((^mf or ^a) : (static member traverseBB : (^a -> ^b) * ^c -> ^d) (f, x))
let inline traverseBB (f : ^a -> ^b) (x : ^c) : ^d
when (Multitraverse or ^c) : (static member traverseBB : (^a -> ^b) * ^c -> ^d) =
// The intent of requiring monad is just trying to be lawful
traverseBB_<Multitraverse,^a,^b,^c,^d> (f, x)
let private maybeZero : int -> Foo<int,int> =
fun x -> Bar(0, 2)
// This type clearly does not match the implementation, and yet it type checks
let private whatInTheWorld : list<string>*int -> System.Random =
traverseBB maybeZeroCompiler like => "Oh yeah this is fine, just go on. I don't see this insane typing :)" |
|
Interesting code 1: type Foo<'a, 'b> = Bar of 'a * 'b
type Multifunctor() =
static member inline mapB (f : ^b -> ^b0, (a : ^a, b : ^b)) : ^a * ^b0 = (a, f b)
static member inline mapB (f : ^b -> ^b0, x : Foo< ^a, ^b0>) = f
let inline mapB_< ^mf, ^f, ^a, ^b when (^mf or ^a) : (static member mapB : ^f * ^a -> ^b)> (f : ^f, x : ^a) : ^b =
((^mf or ^a) : (static member mapB : ^f * ^a -> ^b) (f, x))
type Multitraverse() =
static member inline traverseBB (f : ^b1 -> ^b2, x : ^a1 * ^c2 * ^d3) = fun a -> printfn "hi"; a
static member inline traverseBB (f : ^b -> ^b0, (a : ^a, b : ^b)) : ^b1
when (Multifunctor or ^b0) : (static member mapB : _ * ^b0 -> ^b1) =
mapB_<Multifunctor,_,_,_> ((fun x -> ""), (f b))
let inline traverseBB_< ^mf, ^a, ^b, ^c, ^d when (^mf or ^a) : (static member traverseBB : (^a -> ^b) * ^c -> ^d)> (f : ^a -> ^b, x : ^c) : ^d =
((^mf or ^a) : (static member traverseBB : (^a -> ^b) * ^c -> ^d) (f, x))
let inline traverseBB (f : ^a -> ^b) (x : ^c) : ^d
when (Multitraverse or ^c) : (static member traverseBB : (^a -> ^b) * ^c -> ^d) =
// The intent of requiring monad is just trying to be lawful
traverseBB_<Multitraverse,^a,^b,^c,^d> (f, x)
let private maybeZero : int -> Foo<int,int> =
fun x -> Bar(0, 2)
// This type clearly does not match the implementation, and yet it type checks
let private whatInTheWorld : list<string>*int -> System.Random =
traverseBB maybeZeroreplace Interesting code 2: type Foo<'a, 'b> = Bar of 'a * 'b
type Multifunctor() =
static member inline mapB (f : ^b -> ^b0, (a : ^a, b : ^b)) : ^a * ^b0 = (a, f b)
static member inline mapB (f : ^b -> ^b0, x : Foo< ^a, ^b0>) = f
let inline mapB_< ^mf, ^f, ^a, ^b when (^mf or ^a) : (static member mapB : ^f * ^a -> ^b)> (f : ^f, x : ^a) : ^b =
((^mf or ^a) : (static member mapB : ^f * ^a -> ^b) (f, x))
type Multitraverse() =
static member inline traverseBB (f : ^b1 -> ^b2, x : ^a1 * ^c2 * ^d3) = fun a -> printfn "hi"; a
static member inline traverseBB (f : ^b -> ^b0, (a : ^a, b : ^b)) : ^b1
when (Multifunctor or ^b0) : (static member mapB : _ * ^b0 -> ^b1) =
mapB_<Multifunctor,_,_,_> ((fun x -> 1), (f b))
let inline traverseBB_< ^mf, ^a, ^b, ^c, ^d when (^mf or ^a) : (static member traverseBB : (^a -> ^b) * ^c -> ^d)> (f : ^a -> ^b, x : ^c) : ^d =
((^mf or ^a) : (static member traverseBB : (^a -> ^b) * ^c -> ^d) (f, x))
let inline traverseBB (f : ^a -> ^b) (x : ^c) : ^d
when (Multitraverse or ^c) : (static member traverseBB : (^a -> ^b) * ^c -> ^d) =
// The intent of requiring monad is just trying to be lawful
traverseBB_<Multitraverse,^a,^b,^c,^d> (f, x)
let private maybeZero : int -> Foo<int,int> =
fun x -> Bar(0, 2)
// This type clearly does not match the implementation, and yet it type checks
let private whatInTheWorld : list<string>*int -> System.Random =
traverseBB maybeZeroor replace it with an constant int value and we get a correct compiler error: |
dsyme
added
Area-Compiler-SRTP
Using statically resolved type parameters, we ran into a problem where we wrote some code that was wrong according to what the types said, and yet compiled (and so we didn't realize it was wrong). While writing unit tests against it, we got an
InvalidCastException, which was exceedingly puzzling, because nowhere in our code did we use casting. I have boiled this down to a minimal working example.Repro steps
Provide the steps required to reproduce the problem
Download my minimal working example.
Read the code and comments in
Program.fsto get an idea of what's going on hear.SRTP.fscontains the backing statically resolved type parameter code etc.Compile.
Run the resulting
.exeand observe the output.Expected behavior
Program should not typecheck.
Actual behavior
Depends on what you do with the values that do not match their declared types:
InvalidCastExceptionat runtime explaining that the real type can't be cast to the supposed type.Known workarounds
I can correct my code and get it to work but my only workaround for regaining confidence that code that compiles is correct is to stop using statically resolved type parameters.
Related information
Provide any related information
Please let me know if more detailed information is needed. This is a high priority issue for me as it seriously compromises the integrity of my F# code.
The text was updated successfully, but these errors were encountered: