Quantified Constraints

[Odomontois]

This have basically same motivation and use cases as Haskell Extension with the same name

More idiomatic name: Given Derivations

Basic usage

This feature works on top of implicit function types and polymorphic functions. Having given derivations should allow you to write similar code (syntax may vary):

given [F[_], A](given [B] =>> (given Eq[B]) => Eq[F[B]])): Eq[Free[F, A]]

It's realy useful for generalized recursion as well it makes typeclasses like MonoidK SemigroupK, EqK, OrdK etc. obsolete
Also a whole new space for modularization and library design emerges.

Syntax

In any point where given parameter is suitable it type can be one of the following

// polymorphic function type which result is normal type for Given
[A, B, ...] =>> GivenType[A, B, ...] 

// implicit function type which result is normal type for Given
given(T1, T2) => GivenType

// combination of previous two
[A, B, ...] =>> (given T1[A, B,...], T2[A, B,...]) => GivenType[A, B, ...]

Instance matching

When the instance for

[A] =>> (given Ord[A]) => Ord[Either[String, A]]

is searched, following definitions should match :

//exact match
given [A] (given Ord[A]) : Ord[Either[String, A]]

// context weakening
given [A] : Ord[Either[String, A]]

//context widening
given [A] (given Eq[A]) : Ord[Either[String, A]]

// type application
given [A, B] (given Ord[A], Ord[B]) : Ord[Either[A, B]]

as it expected the applicability of the latter depends on searching for given Ord[String]

Instance generation

Generates instances should be generated and passed as normal lambda functions, closed on additional derived given params of the instance

Instance application

Whenever given Ord[Either[String, Int]] is searched. given function of type

[A] =>> (given Ord[A]) => Ord[Either[String, A]]

if it found in the impicit context should be tried for applicability as if it were defined following way

given [A]  (given Ord[A]): Ord[Either[String, A]]

[neko-kai]

Two other requests for the same: #50 #66