A recent post here inspired me to try and make some changes to the compiler to support more coercions when a type variable is determined by constraints.
The result is a magic compiler solved class called Infer:
class Infer :: forall k. k -> Constraint
class Infer a
When the Infer constraint appears in a type annotation, it tells the compiler to eagerly unambiguously solve for the variables mentioned in the type argument during entailment. This information is then used to introduce Coercible information to allow coerce to be used.
As an example, old can be replaced with new:
old :: forall r
. Coercible r ( hello :: Int, world :: String)
=> Union ( hello :: Int ) ( world :: String ) r
=> Record r
old = coerce { hello: 10, world: "foo" }
new :: forall r
. Infer r
=> Union ( hello :: Int ) ( world :: String ) r
=> Record r
new = coerce { hello: 10, world: "foo" }
Usually the compiler takes Union ( hello :: Int ) ( world :: String ) r as a given in the definition of new, and only when new is used does the compiler try to satisfy that constraint. However, as r has been marked for solving, it tries to solve it within the definition of new, and will raise errors if it cannot.
For example the following would immediately throw an error, as it cannot make a both Int and String:
bad :: forall a. a ~ Int => a ~ String => Infer a => {}
bad = {}
The motivation for this addition is to allow complex types to be generated by classes, these toy examples don’t really make it worth it.
It’s worth noting that even though the variables are solved, they are not removed. This results in constraints getting solved twice, but as they assign the same types to the variables it doesn’t really matter.
Under the hood, we solve the variables by replacing all mentions of it in constraints with a new unification constant, and solve those constraints. An Infer constraint is considered solved when all of the unification constants relating to the variables mentioned have substitutions which have no unification constants or variables that are in any Infer constraints
If you want to build it, make sure to disable warnings:
stack build --fast --ghc-options "-w"