Does not normalize KnownNat for example

[oliver-batchelor]

I'm not sure if I'm doing something dense here - but it does not seem to be having any effect. GHC 8.0.1. ghc-typelits-natnormalize from hackage release 0.5.1

{-# LANGUAGE GADTs, KindSignatures, TypeOperators, PatternGuards , ScopedTypeVariables, TypeFamilies, FlexibleInstances , MultiParamTypeClasses, FlexibleContexts, TypeApplications #-}

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

import Data.Proxy import GHC.TypeLits

test :: (KnownNat n1, KnownNat n2) => Proxy n1 -> Proxy n2 -> Proxy (n1 + n2) test = Proxy

test1 :: forall n. KnownNat n => Proxy n -> Proxy (n * 3) test1 _ = test (test (Proxy :: Proxy n) (Proxy :: Proxy n)) (Proxy :: Proxy n)

Test.hs:15:11: error: • Could not deduce (KnownNat (n + n)) arising from a use of ‘test’ from the context: KnownNat n bound by the type signature for: test1 :: KnownNat n => Proxy n -> Proxy (n * 3)

[christiaanb]

To solve the KnownNat constraint you can use my ghc-typelits-knownnat solver: http://hackage.haskell.org/package/ghc-typelits-knownnat

So:

• ghc-typelits-natnormalise is there to prove equalities between arithmetic expression
• ghc-typelits-knownnat is there to infer "complex" KnownNat constraints from simpler ones

I've decided to keep these functionalities in separate plugins to make the logic and structure of the plugins simpler. For me, this reduces the risk of bugs, where bugs in type-checker plugins can be very harmfull as they can let type-incorrect programs go through.

So no, you weren't doing anything dense at all, it is just my "paranoia" to keep type-checker plugin functionalities sepearte.

[oliver-batchelor]

Oops. I didn't even realize these were different projects and somehow was looking at the wrong one! Thanks!

[christiaanb]

@Saulzar can this issue be closed?

[oliver-batchelor]

Oh yes, of course.