#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