Adam, Somewhat earlier, Adam Gundry wrote:
You might take a look at the rather lovely ghc-typelits-natnormalise plugin. I haven't tried, but assuming you adjust the code to use a type equality constraint rather than CmpNat, I think it should automatically solve the problematic constraint.
The use of ghc-typelits-natnormalise turned out to be a huge success! (modulo the typical z-versus-s issue, that caused some guessing : -) I only made the package available to Cabal, added the one-liner pragma, made the trivial modification you suggested, and the following just worked:
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-} {-# LANGUAGE DataKinds, GADTs, KindSignatures, StandaloneDeriving, TypeOperators, UnicodeSyntax #-}
module Understanding.Types where
import GHC.TypeLits
data T p (size ∷ Nat) where TZ ∷ T p 0 TS ∷ (Show p, (m + 1) ~ n) ⇒ { payload ∷ p , next ∷ T a m } → T a n deriving instance Show p ⇒ Show (T p s)
class MeasuredMonoid a where mmempty ∷ a 0 mmappend ∷ a n → a m → a (n + m)
instance MeasuredMonoid (T p) where mmempty = TZ mmappend TZ TZ = TZ mmappend TZ t@(TS _ _) = t mmappend t@(TS _ _) TZ = t mmappend tl@(TS pl nl) tr = TS pl $ mmappend nl tr
(<>) ∷ MeasuredMonoid a ⇒ a n → a m → a (m + n) (<>) = mmappend
-- * Success, due to use of OPTIONS_GHC -fplugin GHC.TypeLits.Normalise -- > :t TZ <> TZ -- TZ <> TZ :: T p 0 -- > TS 1 TZ <> TS 0 TZ -- TS {payload = 1, next = TS {payload = 0, next = TZ}} -- > :t TS 1 TZ <> TS 0 TZ -- TS 1 TZ <> TS 0 TZ :: T a 2 Thank you, everybody! -- take care, Kosyrev Serge