Let universal quantifier implement instantiate[T] method

[kory33]

Current implementation

∀[F] := ￢[∃[[x] => ￢[F[x]]]]

Why couldn't I define instantiate[T]?

Since scala doesn't support inference of type constructors, I couldn't add implicit class which read the type constructor automatically.

What to do?

• make universal quantifier a class or a trait instead of type alias to ￢[∃[￢[x => F[x]]]]
• let ∀[F] implement ￢[∃[￢[x => F[x]]]]
• define implicit conversion from ￢[∃[￢[x => F[x]]]] to ∀[F]

I'm not yet sure if the last point is possible or not. Most likely it is possible since double negation elimination is at my disposal.

[kory33]

Last one is impossible since the inference for F does not work.

[kory33]

Even if ∀[F] implements ￢[∃[￢[x => F[x]]]], at some point the type constructor has to be explicitly stated between conversions. Unless type constructor inference works in some form, it is entirely impossible to not write a type constructor before generalisation or instantiation.