search

ku-fpg / hermit

Haskell Equational Reasoning Model-to-Implementation Tunnel
http://www.ittc.ku.edu/csdl/fpg/Tools/HERMIT
BSD 2-Clause "Simplified" License
49 stars 8 forks source link

buildDictionaryT and free type variables? #170

Open conal opened 8 years ago

conal commented 8 years ago

Is there an issue with buildDictionaryT and types with free type variables? I had an old guardMsg in my code that uses buildDictionaryT to avoid free type variables (failing when they're present). I now need to build dictionaries even when there are free variables (assuming there's enough known structure to determine an instance), in order to support separate compilation usefully. I'm getting success where I shouldn't, however, and lintExprR is reporting errors like the following:

In the expression: $fNumCat:>a
                     @ a $dNum $dRead $dShow $dEq $dGenBuses $dSourceToBuses
$dNum :: Num a is out of scope

There is a bound type variable a in scope, but perhaps it has a different unique. Moreover, there isn't really enough type information to satisfy these superclass constraints other than Num.

For now, I'm adding a lintExprR call after each buildDictionaryT call, so I'm okay for now, but I'd rather find a cheaper solution.

I'm happy to learn more about the mechanics underlying buildDictionaryT and try sleuthing this one out myself, and I do have a workaround, so no rush on this issue. At this point, I'd appreciate a reminder of the status, and any insights, tips, etc.

conal commented 8 years ago

BTW, I just stumbled onto ghc-tcplugins-extra, as used in Iavor's type-nat-solver. Might be useful with HERMIT.