search

clash-lang / ghc-typelits-natnormalise

Normalise GHC.TypeLits.Nat equations
Other
43 stars 15 forks source link

Inference regression #42

Closed alex404 closed 4 years ago

alex404 commented 4 years ago

Hi there, I just noticed when trying to update my libraries to use stack LTS-15.0 and ghc 8.8.2 (and thus ghc-typelits-natnormalise and knownnat 7.1 and 7.2) that I'm getting a new inference error in my code. In particular, I get

Could not deduce: (Div n (r * c) * (r * c)) ~ ((Div n (r * c) * r) * c)

Dropping down to natnormalise and knownnat 0.7 fixes the problem.

Thanks for all your hardwork on these packages by the way.

leonschoorl commented 4 years ago

Thanks for the report.

Do you have a small example that reproduces this error? I tried doing:

{-# LANGUAGE TypeOperators,NoStarIsType #-}
{-# OPTIONS_GHC -fplugin=GHC.TypeLits.Normalise #-}
import GHC.TypeLits
import Data.Proxy
import Prelude

test1 :: Proxy n -> Proxy r -> Proxy c
      -> Proxy (Div n (r * c) * (r * c))
      -> Proxy ((Div n (r * c) * r) * c)
test1 _ _ _ = id

And that just works using ghc-8.8.2 and ghc-typelits-natnormalise-0.7.1

alex404 commented 4 years ago

Hi, thanks for getting back. I'm completely swamped with work right now, but I'll report back as soon as I find the time to properly investigate.

alex404 commented 4 years ago

So the bug was apparently only triggered by certain type signatures inside a function definition, and when I removed the type signatures everything type checked fine. So it sort of still seems like a bug but not one I can isolate, and one that can be easily avoided. ¯_(ツ)_/¯