search

clash-lang / ghc-typelits-extra

Extra type-level operations on GHC.TypeLits.Nat and a custom solver
Other
16 stars 9 forks source link

Plugin doesn't reduce Min in some cases #7

Closed knupfer closed 7 years ago

knupfer commented 7 years ago

I've got the following minimal usecase which errors out because it doesn't realise that (Min (n+1) n ~ n) I'm developing a library based on your plugins and this is quite an obstacle at the moment.

{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise
                -fplugin GHC.TypeLits.Extra.Solver #-}

{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}

module Bug where

import Data.Proxy
import GHC.TypeLits
import GHC.TypeLits.Extra

x :: Proxy n -> Proxy (Min (n+1) n)
x = id
knupfer commented 7 years ago

Thanks! Keep up the good work