[Haskell-cafe] Typechecker Plugin Constraint Solving

[Armin Wurzinger]

Good day,

I am currently developing a typechecker plugin for GHC for realizing an 
idea
regarding types based on regular expressions to describe the contents of 
a string.
This is done using type-level literals to denote a particular regex. 
Additionally
there are additional constraints for working with such types. One of those
constraints is called Intersectable and denotes whether an intersection 
between
two regexes would be possible in the sense that there is some common 
alphabet
between them. Furthermore there is a type-level function that calculates 
the
actual intersection between two regex types and returns the resulting 
regex type:

type family Intersectable (a :: Symbol) (b :: Symbol) :: Constraint
type family Intersection (a :: Symbol) (b :: Symbol) :: Symbol

Now i've created a typechecker plugin that resolves such constraints by 
using a
finite-automata representation of the regexes to do the actual work. 
While my
plugin is already able to proof progams where regexes are fully applied, 
i.e. they
can reduce terms to a single regex and then verify the constraints 
accordingly
or reject them, it fails to type "intermediate" functions. As a small 
example
assume the following program:

checkFour :: Intersectable a "[0-4]" => RgxString a -> RgxString 
(Intersection a "[0-4]")
checkFour a = undefined

checkEight :: Intersectable a "[0-8]" => RgxString a -> RgxString 
(Intersection a "[0-8]")
checkEight a = undefined

test = checkFour . checkEight  -- this fails to type correctly
test2 = checkFour $ checkEight $ (RgxString :: RegexString ".*") -- this 
works fine

The constraint solver wants me to proof the following constraints for test:

tcPluginSolve
given   = []
derived = []
wanted  = [
[WD] irred_a2GV {0}:: Intersectable
     (Intersection a0 "[0-8]")
     "[0-4]" (CNonCanonical),
[WD] irred_a2GY {0}:: Intersectable a0 "[0-8]" (CNonCanonical)]

My plugin reduces the first constraint to Intersectable a0 [0-4] as regex
intersection is commutative so i can intersect [0-8] with [0-4] first. 
But i
haven't found out yet how i would tell the compiler to put this reduced
constraint to the type signature instead of the current one where the 
constraint
got dropped at all instead of at least remain unnormalized, and the 
return type
remains unnormalized as well:

RgxString a -> RgxString (Intersection (Intersection a "[0-8]") "[0-4]")

I'd need to tell the typechecker somehow that (Intersection
(Intersection a "[0-8]") "[0-4]") is equal to Intersection a "[0-4]" so 
it substitutes
it accordingly. My idea is that i have to generate given type and 
function equality
constraints during the  typechecking telling it that those 
representations are equal,
but i am really not sure what kind of constraints i need. CTyEqCan for 
instance
seems to require a TyVar on one side while i though i could generate 
something like

Intersection (Intersection a "[0-8]") "[0-4]" ~ Intersection a "[0-4]"

I have already tried a lot but there is little documentation on the whole
constraint solving process and i am slowly getting stuck. Thanks for 
helping!
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20180704/e882f654/attachment.html>