search

yav / type-nat-solver

A plugin for solving numeric constraints in GHC's type-checker
Other
50 stars 5 forks source link

Tick-marks in type variable names crash the solver #3

Closed plaidfinch closed 8 years ago

plaidfinch commented 8 years ago

Hi Iavor,

When I use a type variable with a tick-mark (e.g. n') in a place where the solver needs to examine it, I get a crash which looks something like:

*** Exception: user error (Unexpected result from the SMT solver:
  Expected: success
  Result: (error "line 6 column 14: unexpected character" )

A minimal example illustrating this issue:

{-# OPTIONS_GHC -fplugin=TypeNatSolver #-}
module Bug where

import Data.Proxy
import GHC.TypeLits

fails :: Proxy (n' <=? n' + 1) -> ()
fails Proxy = ()

succeeds :: Proxy (n <=? n + 1) -> ()
succeeds Proxy = ()

If fails is left uncommented, the module will throw such an error when compiled.

I'm guessing that this issue could be fixed by sanitizing/unsanitizing names at the boundary of the solver, using some scheme like z-encoding.

If you point me in the direction of where this encoding layer needs to go, I'll gladly go fix it and send a pull request.

yav commented 8 years ago

Ah, good point. The name is chosen in thyVarName if you want to have a go at fixing this.