search

clash-lang / ghc-typelits-knownnat

Derive KnownNat constraints from other KnownNat constraints
Other
14 stars 10 forks source link

Inferred constraint is too strong #19

Closed andygill closed 6 years ago

andygill commented 6 years ago

Consider this example

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ViewPatterns #-}
-- {-# OPTIONS_GHC -fplugin=GHC.TypeLits.KnownNat.Solver #-}

import GHC.TypeLits
import Data.Proxy

type P h kh = h - (kh - 1)

f :: forall h kh . (
--   KnownNat (P h kh),-- uncomment this to manually provide the correct context
    KnownNat h, KnownNat kh) => Integer
f = natVal @(P h kh) Proxy

The plugin infers kh <= h, which is too strong; it should infer kh-1 <= h, or even kh <= h + 1.

christiaanb commented 6 years ago

Ah, I think I know what's going on. The normalising code from ghc-typelits-natnormalise that is used in ghc-typelits-knownnat normalised the type

h - (kh - 1)

to:

1 + (h - kh)

which lead to the kh <= h constraint.

I think when I've properly fixed https://github.com/clash-lang/ghc-typelits-natnormalise/issues/14 I'll be able to fix this bug as well. It will then get as constraints:

1 <= kh, kh-1 <= h

I think the gist of it is: subtraction is annoying when trying to prove things about it.