[GHC] #12102: “Constraints in kinds” illegal family application in instance (+ documentation issues?)
#12102: “Constraints in kinds” illegal family application in instance (+ documentation issues?) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Keywords: TypeInType | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- GHC 8.0.0.20160511. Example from the user guide: [https://downloads.haskell.org/~ghc/8.0.1/docs/html/users_guide/glasgow_exts.... #constraints-in-kinds Constraints in kinds] {{{#!hs type family IsTypeLit a where IsTypeLit Nat = 'True IsTypeLit Symbol = 'True IsTypeLit a = 'False data T :: forall a. (IsTypeLit a ~ 'True) => a -> * where MkNat :: T 42 MkSymbol :: T "Don't panic!" }}} Deriving a standalone `Show` instance *without* the constraint works fine {{{#!hs deriving instance Show (T a) }}} but I couldn't define a `Show` instance given the constraints: {{{#!hs -- • Couldn't match expected kind ‘'True’ -- with actual kind ‘IsTypeLit a0’ -- The type variable ‘a0’ is ambiguous -- • In the first argument of ‘Show’, namely ‘T a’ -- In the stand-alone deriving instance for ‘Show (T a)’ deriving instance Show (T a) }}} let's add constraints {{{#!hs -- • Couldn't match expected kind ‘'True’ -- with actual kind ‘IsTypeLit lit’ -- • In the first argument of ‘Show’, namely ‘T (a :: lit)’ -- In the instance declaration for ‘Show (T (a :: lit))’ instance IsTypeLit lit ~ 'True => Show (T (a :: lit)) where }}} let's derive for a single literal {{{#!hs -- • Illegal type synonym family application in instance: -- T Nat -- ('Data.Type.Equality.C:~ -- Bool -- (IsTypeLit Nat) -- 'True -- ('GHC.Types.Eq# Bool Bool (IsTypeLit Nat) 'True <>)) -- 42 -- • In the stand-alone deriving instance for ‘Show (T (42 :: Nat))’ deriving instance Show (T (42 :: Nat)) }}} same happens with {{{#!hs instance Show (T 42) where }}} ---- The documentation
Note that explicitly quantifying with `forall a` is not necessary here.
seems to be wrong since removing it results in {{{ tVDv.hs:10:17-18: error: … • Expected kind ‘a’, but ‘42’ has kind ‘Nat’ • In the first argument of ‘T’, namely ‘42’ In the type ‘T 42’ In the definition of data constructor ‘MkNat’ Compilation failed. }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12102 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12102: “Constraints in kinds” illegal family application in instance (+ documentation issues?) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * cc: goldfire (added) Comment: I agree that something is quite fishy is going on here—or perhaps several things? The further I dug into this, the more horrified I became. One thing I tried was seeing what GHCi thinks of this engimatic `T` type: {{{ $ ghc/inplace/bin/ghc-stage2 --interactive Bug2.hs GHCi, version 8.3.20170503: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Main ( Bug2.hs, interpreted ) Ok, modules loaded: Main. λ> :i T type role T nominal nominal data T (b :: IsTypeLit a ~ 'True) (c :: a) where MkNat :: T ('Data.Type.Equality.C:~ ('GHC.Types.Eq# <>)) 42 MkSymbol :: T ('Data.Type.Equality.C:~ ('GHC.Types.Eq# <>)) "Don't panic!" -- Defined at Bug2.hs:14:1 }}} ...Oh. Oh my goodness. I don't even know how one is supposed to possibly interpret that (perhaps this is related to #13407?). Something that's particularly strange is that `T` is reported as having //two// type parameters, which is certainly not correct. This might help explain all of your attempts to use `T` were met with confusing errors. Another thing that perplexes me is—should the definition of `T` as it's written in the original example even be accepted? We have: {{{#!hs data T :: forall a. (IsTypeLit a ~ 'True) => a -> * where ... }}} If I'm reading this correctly, this would desugar into something like this, yes? {{{ data (IsTypeLit a ~ 'True) => T (x :: a) = ... }}} If so, shouldn't that require `DatatypeContexts`? Also if so, why on earth is something that requires `DatatypeContexts` in the users' manual? Perhaps this is my inexperience with this feature bleeding through. After all, I didn't even know "type constraints" were a thing until I stumbled upon this ticket. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12102#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12102: “Constraints in kinds” illegal family application in instance (+ documentation issues?) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Description changed by Iceland_jack: @@ -16,1 +16,2 @@ - Deriving a standalone `Show` instance *without* the constraint works fine + Deriving a standalone `Show` instance *without* the constraint `(IsTypeLit + a ~ 'True) => ` works fine New description: GHC 8.0.0.20160511. Example from the user guide: [https://downloads.haskell.org/~ghc/8.0.1/docs/html/users_guide/glasgow_exts.... #constraints-in-kinds Constraints in kinds] {{{#!hs type family IsTypeLit a where IsTypeLit Nat = 'True IsTypeLit Symbol = 'True IsTypeLit a = 'False data T :: forall a. (IsTypeLit a ~ 'True) => a -> * where MkNat :: T 42 MkSymbol :: T "Don't panic!" }}} Deriving a standalone `Show` instance *without* the constraint `(IsTypeLit a ~ 'True) => ` works fine {{{#!hs deriving instance Show (T a) }}} but I couldn't define a `Show` instance given the constraints: {{{#!hs -- • Couldn't match expected kind ‘'True’ -- with actual kind ‘IsTypeLit a0’ -- The type variable ‘a0’ is ambiguous -- • In the first argument of ‘Show’, namely ‘T a’ -- In the stand-alone deriving instance for ‘Show (T a)’ deriving instance Show (T a) }}} let's add constraints {{{#!hs -- • Couldn't match expected kind ‘'True’ -- with actual kind ‘IsTypeLit lit’ -- • In the first argument of ‘Show’, namely ‘T (a :: lit)’ -- In the instance declaration for ‘Show (T (a :: lit))’ instance IsTypeLit lit ~ 'True => Show (T (a :: lit)) where }}} let's derive for a single literal {{{#!hs -- • Illegal type synonym family application in instance: -- T Nat -- ('Data.Type.Equality.C:~ -- Bool -- (IsTypeLit Nat) -- 'True -- ('GHC.Types.Eq# Bool Bool (IsTypeLit Nat) 'True <>)) -- 42 -- • In the stand-alone deriving instance for ‘Show (T (42 :: Nat))’ deriving instance Show (T (42 :: Nat)) }}} same happens with {{{#!hs instance Show (T 42) where }}} ---- The documentation
Note that explicitly quantifying with `forall a` is not necessary here.
seems to be wrong since removing it results in {{{ tVDv.hs:10:17-18: error: … • Expected kind ‘a’, but ‘42’ has kind ‘Nat’ • In the first argument of ‘T’, namely ‘42’ In the type ‘T 42’ In the definition of data constructor ‘MkNat’ Compilation failed. }}} -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12102#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12102: “Constraints in kinds” illegal family application in instance (+ documentation issues?) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): Yeah this is something odd Replying to [comment:1 RyanGlScott]:
Perhaps this is my inexperience with this feature bleeding through. After all, I didn't even know "type constraints" were a thing until I stumbled upon this ticket.
Richard has a paper on [http://cs.brynmawr.edu/~rae/papers/2017/partiality/partiality.pdf Constrained Type Families], which as I understand it might express this with closed type classes who knows {{{#!hs class TypeLit (a :: Type) where instance TypeLit Nat instance TypeLit Symbol data T :: forall a. TypeLit a => a -> Type where MkNat :: T 42 MkSymbol :: T "Don't panic!" }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12102#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12102: “Constraints in kinds” illegal family application in instance (+ documentation issues?) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): I think I found a solution for this particular case, using `TypeFamilyDependencies`, if we make a restricted code {{{#!hs data Code = NAT | SYMBOL }}} with an injective interpretation {{{#!hs type family Interp (a :: Code) = (res :: Type) | res -> a where Interp NAT = Nat Interp SYMBOL = Symbol }}} then you can write {{{#!hs data T :: forall a. Interp a -> Type where MkNat :: T 42 MkSymbol :: T "Don't panic!" deriving instance Show (T a) deriving instance Eq (T a) deriving instance Ord (T a) -- deriving instance Read (T a) }}} but using any of those methods causes the error in #13643 :) once that ticket is created -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12102#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12102: “Constraints in kinds” illegal family application in instance (+ documentation issues?) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): I didn't even know we allowed constraints in kinds. We certainly should not allow lifted equality constraints, like `T :: forall k. (t1 ~ t2) => blah`. Because `(t1 ~ t2)` is represented by lifted, heap-allocated, possibly-bottom value, and we don't have a `case` expression in types to unpack it. Possibly we should allow unlifted equality `T :: forall k. (t1 ~# t2) => blah`. I'm not sure. But what you have is definitely wrong and should be rejected with a decent error message. (And the user manual should be fixed!) Richard what do you think? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12102#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12102: “Constraints in kinds” illegal family application in instance (+ documentation issues?) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Good questions. Here are my thoughts: - Satisfying kind-level equality constraints is implemented in `Inst.tcInstBinderX`, called when a type is applied to some arguments. The code there handles both unboxed equality and boxed equality. - The "no `case`" problem in Simon's comment:5 is quite true. But this is OK, because such an equality constraint can never be a Given: constraints in types can't be used within the same type, but (I believe) these constraints scope only over a type (never a term). - This last point makes these new constraints somewhat like datatype contexts, but one does not desugar into the other. - Clearly, the output from `:info` is horrible. - The "no `forall` needed" is an interaction with CUSKs. This point should be clarified in the manual. - "Constrained type families" interacts poorly with today's story for kind families: constrained type families requires the use of class constraints, but class constraints aren't currently allowed in kinds. It would seem that it's best to implement constrained type families in the context of Dependent Haskell. - Bottom line: this feature is probably a misfire. It ''is'' marginally useful, as I think the example from the manual demonstrates. (That seems useful to me, at least.) But the implementation is very ad-hoc, and the fact that these constraints never appear as Givens take much of the air out of them. It would be easy enough to remove this feature for 8.2. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12102#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12102: “Constraints in kinds” illegal family application in instance (+ documentation issues?) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): I'm still lost. Even if they are wanteds, that still means we are going to get term-level variables appearing in types, at the occurrences of `T`. If you say we can get rid of them, let's get rid of them. Aasp! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12102#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12102: “Constraints in kinds” illegal family application in instance (+ documentation issues?) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj):
If you say we can get rid of them, let's get rid of them. Aasp!
Richard agrees. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12102#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12102: “Constraints in kinds” illegal family application in instance (+ documentation issues?) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #13780 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * related: => #13780 Comment: BTW, I've opened #13780 to track the pretty-printing issue observed in comment:1. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12102#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12102: “Constraints in kinds” illegal family application in instance (+ documentation issues?) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #13780 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): I was just about to do this. But then I had second thoughts. Right now, we take it as a general rule that the following two declarations are the same: {{{#!hs data G1 a where MkG1 :: G1 Bool data G2 a = (a ~ Bool) => MkG2 }}} and indeed this is true today. But if we throw out `~` in kinds, as proposed here, then only `'MkG1` would be usable in a type. `'MkG2` would be an error, violating our general rule. About Givens: GADT pattern-matching in terms must be very fancy, because the GADT pattern-match relates a runtime thing to a compile-time thing. Figuring out how to do this time travel required several PhDs to be earned. On the other hand, GADT pattern-matching in types need not be nearly so advanced, because everything is compile-time. Indeed, GHC's current implementation of type-level GADT pattern-matching is somewhat simplistic, not using Givens at all. (More below, as I'm sure you'll be curious.) So, even though a `~` in a kind never gives rise to a Given, they are still useful and can be matched against in a type family. How type-level GADT pattern matching works: Let's look at an example. {{{#!hs type family F1 (a :: G k) :: k where F1 MkG1 = True }}} This would seem to require fancy GADT pattern matching. After all, we declare that the return kind be `k` for some unknown `k`, and yet we return `True :: Bool`. However, this really works by doing ''kind- matching''. That is, the definition is elaborated to make its kind variables explicit: {{{#!hs type family F1 (k :: Type) (a :: G k) :: k where F1 Bool MkG1 = True }}} Because type families can pattern-match on kinds, this is hunky dory. The ''caller'' is responsible for showing that `k` is really `Bool`. This sounds terrible, though: what has happened to the expressiveness of GADTs? Nothing bad. Of course the caller can figure out what `k` should be, because it has the same information this function does. (This is very different in terms, where a GADT parameter is learned by a ''runtime'' pattern match. No phase distinction in type families!) This trick has its limits, of course: you can't usefully use a constraint of the form `F a ~ G a` in a kind. I do want to fix that some day. But not today. And, in the meantime, it's unclear if I should fix this ticket and violate the general rule at the top of this comment. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12102#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12102: “Constraints in kinds” illegal family application in instance (+ documentation issues?) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #13780 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): I'm confused then on what this ticket is about. Is the plan to keep this feature and fix the bugs reported in the original comment? FWIW, I noticed that even after commit c2417b87ff59c92fbfa8eceeff2a0d6152b11a47, which fixed several ugly pretty- printer bugs that caused things like `'GHC.Types.Eq#` to be printed, a similar pretty-printer bug in this ticket is still //not// fixed on GHC HEAD. For instance, this program: {{{#!hs {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} import Data.Kind import GHC.TypeLits hiding (type (*)) type family IsTypeLit a where IsTypeLit Nat = 'True IsTypeLit Symbol = 'True IsTypeLit a = 'False data T :: forall a. (IsTypeLit a ~ 'True) => a -> * where MkNat :: T 42 MkSymbol :: T "Don't panic!" instance Show (T 42) where }}} Still spits out `'GHC.Types.Eq#`: {{{ $ ghc5/inplace/bin/ghc-stage2 --interactive Bug.hs GHCi, version 8.3.20170725: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Main ( Bug.hs, interpreted ) Bug.hs:21:10: error: • Illegal type synonym family application in instance: T ('Data.Type.Equality.C:~ ('GHC.Types.Eq# <>)) 42 • In the instance declaration for ‘Show (T 42)’ | 21 | instance Show (T 42) where | ^^^^^^^^^^^ }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12102#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12102: “Constraints in kinds” illegal family application in instance (+ documentation issues?) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #13780 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): I think we first need to decide on whether to keep the feature. Once that's settled, then we can look at the other issues (mostly pretty- printing) brought up here. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12102#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12102: “Constraints in kinds” illegal family application in instance (+ documentation issues?) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #13780 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): In GHC HEAD (as of commit 2257a86daa72db382eb927df12a718669d5491f8), you get the following error when compiling the original program: {{{ $ inplace/bin/ghc-stage2 --interactive ../Bug.hs GHCi, version 8.7.20181129: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Main ( ../Bug.hs, interpreted ) ../Bug.hs:15:1: error: • Illegal constraint in a kind: forall a. (IsTypeLit a ~ 'True) => a -> * • In the data type declaration for ‘T’ | 15 | data T :: forall a. (IsTypeLit a ~ 'True) => a -> * where | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^... }}} Which would suggest that this issue is now moot. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12102#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12102: “Constraints in kinds” illegal family application in instance (+ documentation issues?) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #13780, #15872 | Differential Rev(s): Phab:D5397 Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => patch * differential: => Phab:D5397 * related: #13780 => #13780, #15872 Comment: Phab:D5397 wraps things up by removing the outdated users' guide text about this feature, and adding a regression test. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12102#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12102: “Constraints in kinds” illegal family application in instance (+
documentation issues?)
-------------------------------------+-------------------------------------
Reporter: Iceland_jack | Owner: (none)
Type: bug | Status: patch
Priority: normal | Milestone:
Component: Compiler | Version: 8.0.1
Resolution: | Keywords: TypeInType
Operating System: Unknown/Multiple | Architecture:
| Unknown/Multiple
Type of failure: None/Unknown | Test Case:
Blocked By: | Blocking:
Related Tickets: #13780, #15872 | Differential Rev(s): Phab:D5397
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Ryan Scott
#12102: “Constraints in kinds” illegal family application in instance (+ documentation issues?) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.0.1 Resolution: fixed | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | typecheck/should_fail/T12102 Blocked By: | Blocking: Related Tickets: #13780, #15872 | Differential Rev(s): Phab:D5397 Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * testcase: => typecheck/should_fail/T12102 * status: patch => closed * resolution: => fixed * milestone: => 8.8.1 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12102#comment:16 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12102: “Constraints in kinds” illegal family application in instance (+ documentation issues?) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | typecheck/should_fail/T12102 Blocked By: | Blocking: Related Tickets: #13780, #15872 | Differential Rev(s): Phab:D5397 Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: closed => new * resolution: fixed => * milestone: 8.8.1 => Comment: Commit [https://gitlab.haskell.org/ghc/ghc/commit/6cce36f83aec33d33545e0ef2135894d22... 6cce36f83aec33d33545e0ef2135894d22dff5ca] (`Add AnonArgFlag to FunTy`) added back the ability to have equality constraints in kinds. Unfortunately, the issues in the original description persist. Here's one example of the bizarre things that equality constraints in kinds cause: {{{#!hs {-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TypeFamilies #-} module T12102 where import Data.Kind import GHC.TypeLits type family IsTypeLit a where IsTypeLit Nat = 'True IsTypeLit Symbol = 'True IsTypeLit a = 'False data T :: forall a. (IsTypeLit a ~ 'True) => a -> Type where MkNat :: T 42 MkSymbol :: T "Don't panic!" deriving instance Show (T a) }}} {{{ $ ~/Software/ghc/inplace/bin/ghc-stage2 Bug.hs [1 of 1] Compiling T12102 ( Bug.hs, Bug.o ) Bug.hs:21:25: error: • Expecting one more argument to ‘T a’ Expected a type, but ‘T a’ has kind ‘a0 -> *’ • In the first argument of ‘Show’, namely ‘(T a)’ In the stand-alone deriving instance for ‘Show (T a)’ | 21 | deriving instance Show (T a) | ^^^ Bug.hs:21:27: error: • Couldn't match kind ‘*’ with ‘Constraint’ When matching kinds k0 :: * IsTypeLit a0 ~ 'True :: Constraint Expected kind ‘IsTypeLit a0 ~ 'True’, but ‘a’ has kind ‘k0’ • In the first argument of ‘T’, namely ‘a’ In the first argument of ‘Show’, namely ‘(T a)’ In the stand-alone deriving instance for ‘Show (T a)’ | 21 | deriving instance Show (T a) | ^ }}} Huh? Why is GHC claiming that `T a` has kind `a0 -> *`? Well, if you ask GHCi: {{{ λ> :k T T :: (IsTypeLit a ~ 'True) -> a -> * }}} Yikes. Something is clearly wrong here. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12102#comment:17 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12102: “Constraints in kinds” illegal family application in instance (+ documentation issues?) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | typecheck/should_fail/T12102 Blocked By: | Blocking: Related Tickets: #13780, #15872, | Differential Rev(s): Phab:D5397 #16263 | Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * related: #13780, #15872 => #13780, #15872, #16263 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12102#comment:18 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12102: “Constraints in kinds” illegal family application in instance (+ documentation issues?) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | typecheck/should_fail/T12102 Blocked By: | Blocking: Related Tickets: #13780, #15872, | Differential Rev(s): Phab:D5397 #16263 | Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Ryan, there's now an extensive comment in `Note [Constraints in kinds]` in TyCoRep that describes what is supposed to happen for equality constraints in kinds. In the light of that description, could you spare the time to look into this ticket and #15872 to see what needs doing? I think we may need to look at the user manual too. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12102#comment:19 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12102: “Constraints in kinds” illegal family application in instance (+ documentation issues?) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | typecheck/should_fail/T12102 Blocked By: | Blocking: Related Tickets: #13780, #15872, | Differential Rev(s): Phab:D5397 #16263 | Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): I don't think we're on the same page here. This ticket and #15872 demonstrate that constraints in kinds are horribly broken, and that there's no way to profitably use them. I would think that we should fix GHC's treatment of constraints in kinds before we document how they work in the users' manual. Unfortunately, fixing that is far beyond my technical expertise. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12102#comment:20 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12102: “Constraints in kinds” illegal family application in instance (+ documentation issues?) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | typecheck/should_fail/T12102 Blocked By: | Blocking: Related Tickets: #13780, #15872, | Differential Rev(s): Phab:D5397 #16263 | Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Hang on. The Note explains that * equality constraints `(~)` and `(~~)` should be fine; * other constraints like `Eq a` should be illegal; * `(~#)` isn't a constraint at all; see `Note [Types for coercions, predicates, and evidence]` in `TyCoRep` We should both make the user manual reflect this, and fix any bugs (which surely exist). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12102#comment:21 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12102: “Constraints in kinds” illegal family application in instance (+ documentation issues?) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | typecheck/should_fail/T12102 Blocked By: | Blocking: Related Tickets: #13780, #15872, | Differential Rev(s): Phab:D5397 #16263 | Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Replying to [comment:21 simonpj]:
We should both make the user manual reflect this, and fix any bugs (which surely exist).
I'm just pointing out that "make the user manual reflect this" and "fix any bugs" are two actions which require very different sets of abilities. I //might// be able to do the former, but definitely not the latter. Given that, perhaps we should wait until someone with the competency to fix the latter comes along, and then we can update the users' manual at the same time. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12102#comment:22 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC