Compiling with GHC 8.0.1-rc4

[davean]

The below patch allows compiling with GHC 8.0.1-rc4. Sadly it does so via the use of UndecidableInstances. I did not see a quick way to avoid its use since:

class HasDynamicDimension a => HasDimension a where instance (KnownDimension d) => HasDynamicDimension (Dimensional v d a) where type KnownDimension (d :: Dimension) = HasDimension (Proxy d)

leads to the clear loop (expanded):

class HasDynamicDimension a => HasDimension a where instance (HasDimension (Proxy d)) => HasDynamicDimension (Dimensional v d a) where

This patch avoids https://ghc.haskell.org/trac/ghc/ticket/12026

diff --git a/src/Numeric/Units/Dimensional/Dimensions/TypeLevel.hs b/src/Numeric/Units/Dimensional/Dimensions/TypeLevel.hs
index 51e07b4..c52493d 100644
--- a/src/Numeric/Units/Dimensional/Dimensions/TypeLevel.hs
+++ b/src/Numeric/Units/Dimensional/Dimensions/TypeLevel.hs
@@ -38,7 +38,7 @@ where

 import Data.Proxy
 import Numeric.NumType.DK.Integers
-  ( TypeInt (Zero, Pos1, Pos2, Pos3), (+)(), (-)()
+  ( TypeInt (Zero, Pos1, Pos2, Pos3), type (+)(), type (-)()
   , KnownTypeInt, toNum
   )
 import qualified Numeric.NumType.DK.Integers as N
diff --git a/src/Numeric/Units/Dimensional/Dynamic.hs b/src/Numeric/Units/Dimensional/Dynamic.hs
index b48c192..dde9f37 100644
--- a/src/Numeric/Units/Dimensional/Dynamic.hs
+++ b/src/Numeric/Units/Dimensional/Dynamic.hs
@@ -17,6 +17,7 @@ Defines types for manipulation of units and quantities without phantom types for
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE NoImplicitPrelude #-}
 {-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE UndecidableInstances #-}

 module Numeric.Units.Dimensional.Dynamic
 (
@@ -83,7 +84,7 @@ instance (KnownDimension d) => Demotable (Quantity d) where
       -- This implementation is not provided directly inside the instance because it requires ScopedTypeVariables
       -- Placing the signatures inside the instance requires InstanceSigs, which interacts poorly with associated type families
       -- like Dimensional in GHC 7.8.
-      demoteQ :: forall a (d' :: Dimension).KnownDimension d' => AnyQuantity a -> Maybe (Quantity d' a)
+      demoteQ :: forall a (d' :: Dimension). AnyQuantity a -> Maybe (Quantity d' a)
       demoteQ (AnyQuantity dim val) | dim == dim' = Just . Quantity $ val
                                     | otherwise   = Nothing
         where
diff --git a/src/Numeric/Units/Dimensional/Internal.hs b/src/Numeric/Units/Dimensional/Internal.hs
index 6feac7b..0f91717 100644
--- a/src/Numeric/Units/Dimensional/Internal.hs
+++ b/src/Numeric/Units/Dimensional/Internal.hs
@@ -207,11 +207,11 @@ instance (KnownDimension d, Show a, Fractional a) => Show (Quantity d a) where
 --
 -- >>> showIn watt $ (37 *~ volt) * (4 *~ ampere)
 -- "148.0 W"
-showIn :: (KnownDimension d, Show a, Fractional a) => Unit m d a -> Quantity d a -> String
+showIn :: (Show a, Fractional a) => Unit m d a -> Quantity d a -> String
 showIn (Unit n _ y) (Quantity x) | Name.weaken n == nOne = show (x / y)
                                  | otherwise             = (show (x / y)) ++ " " ++ (show n)

-instance (KnownDimension d, Show a) => Show (Unit m d a) where
+instance (Show a) => Show (Unit m d a) where
   show (Unit n e x) = "The unit " ++ show n ++ ", with value " ++ show e ++ " (or " ++ show x ++ ")"

 -- Operates on a dimensional value using a unary operation on values, possibly yielding a Unit.

[dmcclean]

I'm a little bit confused.

Is it the case that the code shouldn't compile on 7.10 because of a loop, but it does because the compiler doesn't notice, and on 8.0.1-rc4 the compiler does notice but notices by panicking on a partial pattern match?

If so, we should dig down to the bottom of why we have a loop and figure out some way to cut it, I guess? But I have to confess that the clear loop isn't clear to me, probably because I just drove all day. Can you break it down for me?

[dmcclean]

It seems like maybe only the changes in b/src/Numeric/Units/Dimensional/Dimensions/TypeLevel.hs are required, and the ones proposed in b/src/Numeric/Units/Dimensional/Dynamic.hs are only needed because of the ones proposed in b/src/Numeric/Units/Dimensional/Internal.hs?

But I'm not sure. Having trouble getting the 8.0.1 release candidate set up on windows.

This is mostly a guess based on thomie's reduction of the minimal test case for 12026 to just an import statement with an empty paren-list after it like the one that appears on the changed line in TypeLevel.hs?

[davean]

The changes in TypeLevel.hs are required because GHC got more picky about namespaces, and types are different namespace. It must always be specified now. The code previously crashed GHC, as per the bug, but this does not.

UndecidableInstances is required, to avoid:

src/Numeric/Units/Dimensional/Dynamic.hs:79:10: error:
    • The constraint ‘KnownDimension d’
        is no smaller than the instance head
      (Use UndecidableInstances to permit this)
    • In the instance declaration for ‘Demotable (Quantity d)’

The type signature changes are just warning cleanups since the instances were not used. They are completely unrelated to either bug.

Does that help?

[davean]

I'm afraid I can't help you get GHC running on windows - I've never run GHC on windows, nor do I believe I know anyone who has. I may be able to provide you access to a Linux box with GHC 8.0.1-rc4 installed though for the purposes of patching this library (and others) in preparation for the release.

Please let me know if that would expedite progress.

[dmcclean]

It runs fine on Windows, it just is a black art to install until they come out with the official binaries. That would help. I have a virtual box at home but I'm traveling in Pennsylvania.

So the changes to Dynamic.hs are unrelated to the ones in TypeLevel.hs? The TypeLevel.hs ones are definitely unobjectionable.

I'm just trying to get a handle on how the undecidable instances requirement arose, since it compiles fine on 7.8 and 7.10 and makes sense in my head. I'm having trouble seeing where it loops.

[davean]

We have the current definitions in the existing code:

class HasDynamicDimension a => HasDimension a where
instance (KnownDimension d) => HasDynamicDimension (Dimensional v d a) where
type KnownDimension (d :: Dimension) = HasDimension (Proxy d)

If we expand KnownDimension on HasDimension, we get:

class HasDynamicDimension a => HasDimension a where
instance (HasDimension (Proxy d)) => HasDynamicDimension (Dimensional v d a) where

So, the class HasDimension depends on HasDynamicDimension but the instance HasDynamicDimension (Dimensional v d a) depends on HasDimension, which depends on HasDynamicDimension. What order can we instantiate these in that everything is defined before we use it?

PS: See email for your login.

[dmcclean]

Thanks, will get to work on that now briefly and more at the airport tomorrow.

I think that isn't really a loop, because the class HasDimension doesn't really "depend on" HasDynamicDimension, it instead requires an instance of HasDynamicDimension to create an instance of HasDimension. To create the instance for HasDynamicDimension (Dimensional v d a) we have to supply an instance for HasDimension (Proxy d), which in turn requires supplying an instance for HasDynamicDimension (Proxy d) (note, not one for HasDynamicDimension (Dimensional v d a), which was the original demand), which in turn does not require supplying any instances and thus is not a loop. That is how it appears to me to work on 7.10.3 and 7.8.4, without undecidable instances. Those instances are all usable when compiled there.

[dmcclean]

This error you mentioned above:

src/Numeric/Units/Dimensional/Dynamic.hs:79:10: error:
    • The constraint ‘KnownDimension d’
        is no smaller than the instance head
      (Use UndecidableInstances to permit this)
    • In the instance declaration for ‘Demotable (Quantity d)’

seems inaccurate? The constraint KnownDimension d expands to HasDimension (Proxy d). How is that no smaller than the instance head Quantity d = Dimensional 'DQuantity d? I guess I don't know what the language lawyer definition of "smaller" here is, but it seems OK in the sense that we can make progress without guessing, because we erased the bits about Dimensional and 'DQuantity and now we just need to go off and investigate HasDimension (Proxy d), which will lead us to https://github.com/bjornbm/dimensional/blob/master/src/Numeric/Units/Dimensional/Dimensions/TypeLevel.hs#L144-L151, and this appears to be how 7.8.4 and 7.10.3 proceed.

I'm digging through the GHC change list to try to figure out what bug in 7.10 we were exploiting to get away with this that they have shut down.

Thanks again for taking the time to report this and dig in to it! I hope dimensional has been helpful to your work in some way.

[dmcclean]

On to an intriguing clue, will update in 10 minutes when a travis build finishes.

[dmcclean]

I had a thought that perhaps I had incidentally changed some of this machinery in my fixed-point branch (see https://github.com/dmcclean/dimensional/tree/fixed-point) which I am aiming to include in the next release (see #135 to weigh in on whether this is a good idea). Thinking that if I had it might provide insight or an alternative to undecidable instances, I took a look.

Looking at the diff in that PR (which I just updated to fix the type namespace issue) there I don't see any changes to HasDimension, KnownDimension, or HasDynamicDimension or the instance (KnownDimension d) => HasDimension (Dimensional v d a) (except for change to the definition of the kind of v). But it builds and passes tests on the box you provided. (Lots of warnings about the redundant constraints on various functions, but look past those.)

Either I'm missing something obvious in the diff or something is fishy with the release candidate. It's probably the former but I really don't see it.

[dmcclean]

See https://ghc.haskell.org/trac/ghc/ticket/12040 where I reported this even though I'm still not sure what's going on, just in case it is an issue with the release candidate.

[cartazio]

pretty sure any problems in rc4 are also in 8.0.1, which has been cut recently :), or at least the source tarballs are.

also exact-pi and numtype-dk definitely definitely dont build on 8.0.1 :)

[dmcclean]

Thanks for the heads up regarding exact-pi, @cartazio. That should be fixed by v0.4.1.2 that just went up. Also the numtype-dk fix suggested by @davean just went up as v0.5.0.1.

Can you weigh in at all on what's going on with dimensional itself on GHC 8 (if you try to build it against those new versions of numtype-dk and exact-pi? Trying to determine if the issue is ours or theirs, and either way what the best interim fix is. (We may need a long term fix, too, if the issue is ours and GHC 8 remains mistaken in continuing to accept the code in our fixed-point branch #135.)

[cartazio]

Sure thing. If I don't get to it later today please give me a nudge. There's definitely been some changes in ghc that seem to make fancy constraint solving act differently and I've run into them myself

On Monday, May 16, 2016, Douglas McClean notifications@github.com wrote:

Thanks for the heads up regarding exact-pi, @cartazio https://github.com/cartazio. That should be fixed by v0.4.1.2 that just went up. Also the numtype-dk fix suggested by @davean https://github.com/davean just went up as v0.5.0.1.

Can you weigh in at all on what's going on with dimensional itself on GHC 8 (if you try to build it against those new versions of numtype-dk and exact-pi? Trying to determine if the issue is ours or theirs, and either way what the best interim fix is. (We may need a long term fix, too, if the issue is ours and GHC 8 remains mistaken in continuing to accept the code in our fixed-point branch #135 https://github.com/bjornbm/dimensional/pull/135.)

— You are receiving this because you were mentioned. Reply to this email directly or view it on GitHub https://github.com/bjornbm/dimensional/issues/157#issuecomment-219426996

[dmcclean]

Thanks Carter! There are links to the exact commits in question and a writeup of what I find confusing about it at https://ghc.haskell.org/trac/ghc/ticket/12040.

[dmcclean]

This has been addressed by the release of version 1.0.1.2 on hackage.

It will be addressed in the master branch by ongoing discussion in the GHC trac thread and by eventually doing the fixed-point branch (which for mysterious reasons works).

[cartazio]

What differs between master and That version?

On Thursday, May 19, 2016, Douglas McClean notifications@github.com wrote:

This has been addressed by the release of version 1.0.1.2 on hackage.

It will be addressed in the master branch by ongoing discussion in the GHC trac thread and by eventually doing the fixed-point branch (which for mysterious reasons works).

— You are receiving this because you were mentioned. Reply to this email directly or view it on GitHub https://github.com/bjornbm/dimensional/issues/157#issuecomment-220462834

[dmcclean]

A ton of stuff, master is almost ready to be 1.1. That Demoteable type doesn't exist in 1.0.1.2. Also not sure if the HasDynamicDimension machinery does either. Will check later. On May 19, 2016 7:14 PM, "Carter Tazio Schonwald" notifications@github.com wrote:

What differs between master and That version?

On Thursday, May 19, 2016, Douglas McClean notifications@github.com wrote:

This has been addressed by the release of version 1.0.1.2 on hackage.

It will be addressed in the master branch by ongoing discussion in the GHC trac thread and by eventually doing the fixed-point branch (which for mysterious reasons works).

— You are receiving this because you were mentioned. Reply to this email directly or view it on GitHub < https://github.com/bjornbm/dimensional/issues/157#issuecomment-220462834>

— You are receiving this because you commented. Reply to this email directly or view it on GitHub https://github.com/bjornbm/dimensional/issues/157#issuecomment-220472958

[dmcclean]

So now that 1.0.1.2 is fixed, master has just been fixed by merging #135. I'd still love to know what exactly it is in the #135 diff that made this go from not-working to working, but on another level maybe it doesn't matter. I agree with rwbarton's analysis in the GHC trac thread that the problem is just different behavior in the instance termination checker, and that our instances do terminate and it's just a question of whether GHC can prove it.