[GHC] #12040: Code that builds on 7.8.4 and 7.10.3 but fails with requiring UndecidableInstances on 8.0.1-rc4

#12040: Code that builds on 7.8.4 and 7.10.3 but fails with requiring UndecidableInstances on 8.0.1-rc4 -------------------------------------+------------------------------------- Reporter: dmcclean | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Keywords: | Operating System: Linux Architecture: | Type of failure: GHC rejects Unknown/Multiple | valid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- (I am not sure if this is an issue with the release candidate or with my code. I'm sorry, I've tried hard to investigate that but not come to a firm conclusion. I'm reporting it on the chance that it might be an issue with the release candidate.) The code at https://github.com/bjornbm/dimensional/tree/c5b41bbcecb710d566f8af6e561dcafd... builds and passes tests on 7.8.4 and 7.10.3. The same code fails under 8.0.1-rc4 with the following message: {{{ 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)’ }}} I'm not sure if the relationship here between `Demotable`, `KnownDimension`, `HasDimension`, and `HasDynamicDimension` in fact requires undecidable instances (in which case 7.8.4 and 7.10.3 are either allowing it in error? or helpfully allowing it even though they aren't obligated to?) or if it does not in fact require undecidable instances (in which case 8.0.1-rc4 is disallowing it in error). Making things even more interesting, a new feature branch of the same project doesn't appear to change any of the things that should be relevant to this error message, but compiles and tests without the error on 8.0.1-rc4 as well as the earlier compiler versions. That one's at https://github.com/dmcclean/dimensional/tree/9f3b0a207258851964defd90ce497e7.... -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12040 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12040: Code that builds on 7.8.4 and 7.10.3 but fails with requiring UndecidableInstances on 8.0.1-rc4 -------------------------------------+------------------------------------- Reporter: dmcclean | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Linux | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bjornbm): * cc: bjorn.buckwalter@… (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12040#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12040: Code that builds on 7.8.4 and 7.10.3 but fails with requiring UndecidableInstances on 8.0.1-rc4 -------------------------------------+------------------------------------- Reporter: dmcclean | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: Operating System: Linux | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by thomie): * component: Compiler => Compiler (Type checker) Comment: Here is a reduced testcase, without any dependencies. {{{#!hs {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE TypeFamilies #-} module T12040 where import Data.Proxy -- src/Numeric/Units/Dimensional/Variant.hs data Variant = DQuantity -- src/Numeric/Units/Dimensional/Internal.hs class KnownVariant (v :: Variant) where data Dimensional v :: Dimension -> * -> * instance KnownVariant 'DQuantity where newtype Dimensional 'DQuantity d a = Quantity a type Quantity = Dimensional 'DQuantity -- ' -- src/Numeric/Units/Dimensional/Dimensions/TypeLevel.hs data Dimension = Dim -- TypeInt TypeInt TypeInt TypeInt TypeInt TypeInt TypeInt class HasDynamicDimension a where class HasDynamicDimension a => HasDimension a where type KnownDimension (d :: Dimension) = HasDimension (Proxy d) -- src/Numeric/Units/Dimensional/Dynamic.hs class Demotable (q :: * -> *) where instance (KnownDimension d) => Demotable (Quantity d) where }}} {{{ $ ghc-7.10.3 T12040.hs -v0 # ok $ ghc-8.0.1 T12040.hs -v0 T12040.hs:45: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)’ }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12040#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12040: Code that builds on 7.8.4 and 7.10.3 but fails with requiring UndecidableInstances on 8.0.1-rc4 -------------------------------------+------------------------------------- Reporter: dmcclean | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: Operating System: Linux | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by dmcclean): Thanks thornie. Do you have a position on whether the issue is with 7.10.3 being too permissive or 8.0.1 being too restrictive? Beyond "it makes sense to me" and "it used to work", I don't have a good handle on how to go about deciding whether this code is actually in line with the rules. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12040#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12040: Code that builds on 7.8.4 and 7.10.3 but fails with requiring UndecidableInstances on 8.0.1-rc4 -------------------------------------+------------------------------------- Reporter: dmcclean | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: Operating System: Linux | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by rwbarton): It has something to do with the polykindedness of `Proxy`. This further- reduced version displays the same behavior but after replacing `Proxy` by `Maybe`, both versions of ghc accept the program. {{{ {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE KindSignatures #-} module T12040 where import Data.Proxy newtype Dimensional c d a = Quantity a class HasDimension a class Demotable (q :: * -> *) instance (HasDimension (Proxy d)) => Demotable (Dimensional Int d) where }}} Maybe a consequence of kind and type arguments being treated uniformly in GHC's Core language now? Arguably neither behavior is wrong, since the instance termination checker is necessarily a conservative approximation. There's no real harm in just turning on UndecidableInstances. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12040#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12040: Code that builds on 7.8.4 and 7.10.3 but fails with requiring UndecidableInstances on 8.0.1-rc4 -------------------------------------+------------------------------------- Reporter: dmcclean | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: Operating System: Linux | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * cc: goldfire (added) Comment: Adding Richard as this is his area of expertise. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12040#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12040: Code that builds on 7.8.4 and 7.10.3 but fails with requiring UndecidableInstances on 8.0.1-rc4 -------------------------------------+------------------------------------- Reporter: dmcclean | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: Operating System: Linux | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj):
Maybe a consequence of kind and type arguments being treated uniformly in GHC's Core language now?
Yes, probably. Writing the kind argument in we get {{{ instance (HasDimension (Proxy * d)) => Demotable (Dimensional Int d) where }}} and now indeed the bit before the arrow doesn't look smaller than the thing after. I think the solution here is to use `UndecideableInstances`. One could wonder about some kind-aware size metric might be better --- but I don't know what it would be. I'm inclined to say "wont-fix"; but if someone has a better size-metric proposal, go propose it. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12040#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12040: Code that builds on 7.8.4 and 7.10.3 but fails with requiring UndecidableInstances on 8.0.1-rc4 -------------------------------------+------------------------------------- Reporter: dmcclean | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: Operating System: Linux | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by dmcclean): Won't-fix is fine by me. I reported it because I had no idea what was going on and was surprised by the change. In the intervening time we have changed our approach to this part of the code anyway, and as it happens the new code works on GHC 8 without UndecidableInstances anyway. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12040#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12040: Code that builds on 7.8.4 and 7.10.3 but fails with requiring UndecidableInstances on 8.0.1-rc4 -------------------------------------+------------------------------------- Reporter: dmcclean | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: Operating System: Linux | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by dmcclean): I forgot to add: Thanks very much for investigating this, it's good to know what the cause was. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12040#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12040: Code that builds on 7.8.4 and 7.10.3 but fails with requiring UndecidableInstances on 8.0.1-rc4 -------------------------------------+------------------------------------- Reporter: dmcclean | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: invalid | Keywords: Operating System: Linux | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * status: new => closed * resolution: => invalid Comment: OK -- thanks for raising it though. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12040#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC