Compiler sometimes suggests constraints that are impossible to write

[drvink]

Complex SRTP use often leads to the compiler complaining that you need to add a constraint that's syntactically invalid.

#light "off"
module Functor

open System

let inline konst x _ = x

type CFunctor = class
  static member inline fmap (f : ^a -> ^b, a : ^a list) = List.map f a
  static member inline fmap (f : ^a -> ^b, a : ^a option) =
    match a with
    | None -> None
    | Some x -> Some (f x)

  // default implementation of replace
  static member inline replace< ^a, ^b, ^c, ^d, ^e when
      ^a :> CFunctor and
      (^a or ^d) : (static member fmap : (^b -> ^c) * ^d -> ^e) >
      (a, f) =
    ((^a or ^d) : (static member fmap : (^b -> ^c) * ^d -> ^e) (konst a, f))

  // call overridden replace if present
  static member inline replace< ^a, ^b, ^c when
      ^b : (static member replace : ^a * ^b -> ^c)>
      (a : ^a, f : ^b) =
    (^b : (static member replace : ^a * ^b -> ^c) (a, f))
end

let inline replace_instance< ^a, ^b, ^c, ^d when
    (^a or ^c) : (static member replace : ^b * ^c -> ^d)>
    (a : ^b, f : ^c) =
  ((^a or ^c) : (static member replace : ^b * ^c -> ^d) (a, f))

let inline fmap_instance< ^a, ^b, ^c, ^d, ^e when
    (^a or ^d) : (static member fmap : (^b -> ^c) * ^d -> ^e)>
    (f : ^b -> ^c, a : ^d) =
  ((^a or ^d) : (static member fmap : (^b -> ^c) * ^d -> ^e) (f, a))

let inline fmap (f : ^a -> ^b) (a : ^c) =
  fmap_instance<CFunctor, _, _, _, _> (f, a)

let inline replace (a : ^a) (f : ^b) =
  replace_instance<CFunctor, _, _, _> (a, f)

(*
type test(arg : string) = class
  member __.data = arg
  static member inline fmap (f : char -> char, a : test) = String.map f a.data
  static member inline replace (a : char, f : test) = test.fmap (konst a, f)
end

let _ =
  printfn "%A" <| fmap id [1;2;3];
  printfn "%A" <| replace 5 [1;2;3];
  printfn "%A" <| fmap ((+) 1) (Some 2);
  printfn "%A" <| replace 'q' (test("HI"))
 *)

An attempt at writing a signature file for this code would go something like this:

module Functor

val inline konst : x:'a -> 'b -> 'a
type CFunctor =
  class
    static member inline fmap : f:( ^a ->  ^b) * a: ^a list ->  ^b list
    static member inline fmap : f:( ^a ->  ^b) * a: ^a option ->  ^b option
    static member inline replace< ^a, ^b, ^c, ^d, ^e when
                                'a :> CFunctor and
                                ('a or 'd) : (static member fmap : ('b -> 'c) * 'd -> 'e)>
       : a:'c * f:'d -> 'e when
       ('a or 'd) : (static member fmap : ('b -> 'c) * 'd -> 'e)
       and 'a :> CFunctor
    static member inline replace< ^a, ^b, ^c when
                                'b : (static member replace : 'a * 'b -> 'c)>
      : a:'a * f:'b -> 'c when
      'b : (static member replace : 'a * 'b -> 'c)
  end
val inline replace_instance< ^a, ^b, ^c, ^d when
                           ( ^a or  ^c) : (static member replace :  ^b *  ^c ->  ^d)>
  : a: ^b * f: ^c ->  ^d
val inline fmap_instance< ^a, ^b, ^c, ^d, ^e when
                        ( ^a or  ^d) : (static member fmap : ( ^b ->  ^c) *  ^d ->  ^e)>
  : f:( ^b ->  ^c) * a: ^d ->  ^e
val inline fmap< ^a, ^b, ^c, ^d when
(* problem! *) (CFunctor or ^c) : (static member fmap : ( ^a ->  ^b) *  ^c -> ^d)>
  : f:( ^a ->  ^b) -> a: ^c ->  ^d
val inline replace< ^a, ^b, ^d when
(* problem! *)    (CFunctor or ^b) : (static member replace :  ^a *  ^b ->  ^d)>
  : a: ^a -> f: ^b ->  ^d

The problem is that the compiler will complain that you need a signature like val inline fmap< ^a, ^b, ^c, ^d when (CFunctor or ^c) : (static member fmap : ( ^a -> ^b) * ^c -> ^d)>, but that's syntactically invalid because of CFunctor. (Sometimes you have to write a constraint like this within a source file, so the issue is not limited to just signature files.) Sorry for the crazy example--I don't have a smaller one on hand at the moment, though it's certainly possible to trigger with simpler cases.

There are other issues similar to this as well, such as the compiler telling you to add a constraint with an anonymous type variable (like ^?12345).

[dsyme]

Thanks @drvink - I'm labelling this as a suggestion, since strictly speaking it's according to spec. I agree the language restriction should ideally be lifted though. I believe there's a fslang.uservoice.com entry for this, could you take a look?

[drvink]

A quick search for "constraint" didn't turn up anything obvious. The closest things I could find were a different constraint issue and this SO question relating to it.

[dsyme]

Entered here: https://fslang.uservoice.com/forums/245727-f-language/suggestions/7887270-allow-all-inferrable-srtp-constraints-to-be-writte

Closing this issue as it is now a suggestion.