<html>
  <head>

    <meta http-equiv="content-type" content="text/html; charset=utf-8">
  </head>
  <body text="#000000" bgcolor="#FFFFFF">
    <p>
    </p>
    <div class="moz-text-flowed" style="font-family: -moz-fixed;
      font-size: 14px;" lang="x-western">Good day,
      <br>
      <br>
      I am currently developing a typechecker plugin for GHC for
      realizing an idea
      <br>
      regarding types based on regular expressions to describe the
      contents of a string.
      <br>
      This is done using type-level literals to denote a particular
      regex. Additionally
      <br>
      there are additional constraints for working with such types. One
      of those
      <br>
      constraints is called Intersectable and denotes whether an
      intersection between
      <br>
      two regexes would be possible in the sense that there is some
      common alphabet
      <br>
      between them. Furthermore there is a type-level function that
      calculates the
      <br>
      actual intersection between two regex types and returns the
      resulting regex type:
      <br>
      <br>
      type family Intersectable (a :: Symbol) (b :: Symbol) ::
      Constraint
      <br>
      type family Intersection (a :: Symbol) (b :: Symbol) :: Symbol
      <br>
      <br>
      Now i've created a typechecker plugin that resolves such
      constraints by using a
      <br>
      finite-automata representation of the regexes to do the actual
      work. While my
      <br>
      plugin is already able to proof progams where regexes are fully
      applied, i.e. they
      <br>
      can reduce terms to a single regex and then verify the constraints
      accordingly
      <br>
      or reject them, it fails to type "intermediate" functions. As a
      small example
      <br>
      assume the following program:
      <br>
      <br>
      checkFour :: Intersectable a "[0-4]" => RgxString a ->
      RgxString (Intersection a "[0-4]")
      <br>
      checkFour a = undefined
      <br>
      <br>
      checkEight :: Intersectable a "[0-8]" => RgxString a ->
      RgxString (Intersection a "[0-8]")
      <br>
      checkEight a = undefined
      <br>
      <br>
      test = checkFour . checkEight  -- this fails to type correctly
      <br>
      test2 = checkFour $ checkEight $ (RgxString :: RegexString ".*")
      -- this works fine
      <br>
      <br>
      The constraint solver wants me to proof the following constraints
      for test:
      <br>
      <br>
      tcPluginSolve
      <br>
      given   = []
      <br>
      derived = []
      <br>
      wanted  = [
      <br>
      [WD] irred_a2GV {0}:: Intersectable
      <br>
          (Intersection a0 "[0-8]")
      <br>
          "[0-4]" (CNonCanonical),
      <br>
      [WD] irred_a2GY {0}:: Intersectable a0 "[0-8]" (CNonCanonical)]
      <br>
      <br>
      My plugin reduces the first constraint to Intersectable a0 [0-4]
      as regex
      <br>
      intersection is commutative so i can intersect [0-8] with [0-4]
      first. But i
      <br>
      haven't found out yet how i would tell the compiler to put this
      reduced
      <br>
      constraint to the type signature instead of the current one where
      the constraint
      <br>
      got dropped at all instead of at least remain unnormalized, and
      the return type
      <br>
      remains unnormalized as well:
      <br>
      <br>
      RgxString a -> RgxString (Intersection (Intersection a "[0-8]")
      "[0-4]")
      <br>
      <br>
      I'd need to tell the typechecker somehow that (Intersection
      <br>
      (Intersection a "[0-8]") "[0-4]") is equal to Intersection a
      "[0-4]" so it substitutes
      <br>
      it accordingly. My idea is that i have to generate given type and
      function equality
      <br>
      constraints during the  typechecking telling it that those
      representations are equal,
      <br>
      but i am really not sure what kind of constraints i need. CTyEqCan
      for instance
      <br>
      seems to require a TyVar on one side while i though i could
      generate something like
      <br>
      <br>
      Intersection (Intersection a "[0-8]") "[0-4]" ~ Intersection a
      "[0-4]"
      <br>
      <br>
      I have already tried a lot but there is little documentation on
      the whole
      <br>
      constraint solving process and i am slowly getting stuck. Thanks
      for helping!
      <br>
    </div>
  </body>
</html>