Language.Fixpoint.Solver.UniqifyKVars

This module creates new bindings for each argument of each kvar. It also makes sure that all arguments to each kvar are explicit.

For example,

``` bind 0 x bind 1 v constraint: env [0; 1] rhs $k_42 // implicit substitutions [x:=x], [v:=v] wf: env [0] reft {v : int | [$k_42]} ```

becomes

``` bind 0 x bind 1 v bind 2 lq_karg$x$k_42 constraint: env [0; 1] rhs $k_42[lq_karg$x$k_42:=x][lq_karg$v$k_42:=v]

wf: env [2] reft {lq_karg$v$k_42 : int | [$k_42]} ```

Documentation

wfcUniqify :: SInfo a -> SInfo a