Shapeless Generic, strategically like strategic term rewriting, strongly typed with first class polymorphic functions?

I would like to find a way to create a Kiama library, an added function that would have to strictly type the rewrite rules. (Kiama's eveyrything has a term, and the rewrite rules are Term => Option [Term]

I know that shapeless allows you to convert arbitrary case class hierarchies to the sum of product presentation using hlists behind the scenes.

Based on this general view, I believe it is entirely possible to write a generic library of traverse combinators (strategist style) to apply rewrite rules in a generic version of a term consisting of a nested case classe.

I get the feeling that it is possible to use the formless polyN functions to encode polymorphic term rewrite rules that would yield exact types, however, these rewrite rules would have to work with Hlists representing case classes, which can be quite cumbersome compared to how pattern matching allows matching and transforming auxiliary trees

Simple example: this

sealed abstract trait Expr { type Repr }
sealed abstract trait BoolExpr extends Expr { type Repr = Boolean }
sealed abstract trait IntExpr extends Expr { type Repr = Int }
case class BoolVar(sym: Symbol) extends BoolExpr
case class Not( l: BoolExpr ) extends BoolExpr
case class And( l: BoolExpr, r: IntExpr ) extends BoolExpr
case class Or( l: BoolExpr, r: IntExpr ) extends BoolExpr 
case class IntIte( cond: BoolExpr, thenExpr: IntExpr, elseExpr: IntExpr) extends IntExpr
case class IntConst( value: Int ) extends IntExpr
case class IntVar( sym: Symbol ) extends IntExpr

rule1 { case Not(Not(e)) => Some(e) }

rule2 { case IntIte(Not(c), t, e) => Some( IntIte(c, e, t) }

      

        
        
        
      

    

Better yet would be a rewrite system working on GADT Expr [T], where T is the type of the expression and the rewrite rules preserve T. Best wishes.

How possible is this for you?