[GHC] #12553: Reference kind in a type instance declaration defined in another instance declaration
#12553: Reference kind in a type instance declaration defined in another instance declaration -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Old code: {{{#!hs data Full :: Type -> Type data AST :: (Type -> Type) -> (Type -> Type) -- ASTF :: (Type -> Type) -> (Type -> Type) type ASTF dom a = AST dom (Full a) class Syntactic a where type Domain a :: Type -> Type type Internal a :: Type desugar :: a -> ASTF (Domain a) (Internal a) sugar :: ASTF (Domain a) (Internal a) -> a }}} ---- New code with richer kinds {{{#!hs data Sig a = Full a | a :-> Sig a data AST :: (Sig a -> Type) -> (Sig a -> Type) data Sig a = Full a | a :-> Sig a -- ASTF :: (Sig a -> Type) -> (a -> Type) type ASTF dom a = AST dom (Full a) class Syntactic a where type Domain a :: Sig Type -> Type type Internal a :: Type desugar :: a -> ASTF (Domain a) (Internal a) sugar :: ASTF (Domain a) (Internal a) -> a }}} As the type of `ASTF` hints at it could accept arguments of kind `Sig a -> Type` and `a`. I would like to reference the variable `a` from the kind of `Domain` in the kind of `Internal`, but this fails: {{{#!hs -- • Kind variable ‘u’ is implicitly bound in datatype -- ‘Internal’, but does not appear as the kind of any -- of its type variables. Perhaps you meant -- to bind it (with TypeInType) explicitly somewhere? -- Type variables with inferred kinds: a -- • In the class declaration for ‘Syntactic’ class Syntactic a where type Domain a :: Sig u -> Type type Internal a :: u desugar :: a -> ASTF (Domain a) (Internal a) sugar :: ASTF (Domain a) (Internal a) -> a }}} ---- Should the `u` in the kind of `Domain a` be quantified over (which makes this compile)? {{{#!hs type Domain a :: forall k. Sig k -> Type }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12553 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12553: Reference kind in a type instance declaration defined in another instance declaration -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: 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: @@ -65,0 +65,2 @@ + + **Edit**: This doesn't work. New description: Old code: {{{#!hs data Full :: Type -> Type data AST :: (Type -> Type) -> (Type -> Type) -- ASTF :: (Type -> Type) -> (Type -> Type) type ASTF dom a = AST dom (Full a) class Syntactic a where type Domain a :: Type -> Type type Internal a :: Type desugar :: a -> ASTF (Domain a) (Internal a) sugar :: ASTF (Domain a) (Internal a) -> a }}} ---- New code with richer kinds {{{#!hs data Sig a = Full a | a :-> Sig a data AST :: (Sig a -> Type) -> (Sig a -> Type) data Sig a = Full a | a :-> Sig a -- ASTF :: (Sig a -> Type) -> (a -> Type) type ASTF dom a = AST dom (Full a) class Syntactic a where type Domain a :: Sig Type -> Type type Internal a :: Type desugar :: a -> ASTF (Domain a) (Internal a) sugar :: ASTF (Domain a) (Internal a) -> a }}} As the type of `ASTF` hints at it could accept arguments of kind `Sig a -> Type` and `a`. I would like to reference the variable `a` from the kind of `Domain` in the kind of `Internal`, but this fails: {{{#!hs -- • Kind variable ‘u’ is implicitly bound in datatype -- ‘Internal’, but does not appear as the kind of any -- of its type variables. Perhaps you meant -- to bind it (with TypeInType) explicitly somewhere? -- Type variables with inferred kinds: a -- • In the class declaration for ‘Syntactic’ class Syntactic a where type Domain a :: Sig u -> Type type Internal a :: u desugar :: a -> ASTF (Domain a) (Internal a) sugar :: ASTF (Domain a) (Internal a) -> a }}} ---- Should the `u` in the kind of `Domain a` be quantified over (which makes this compile)? {{{#!hs type Domain a :: forall k. Sig k -> Type }}} **Edit**: This doesn't work. -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12553#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12553: Reference kind in a type instance declaration defined in another instance declaration -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: 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): If I constrain the types `Domain a :: Sig Type -> Type`, `Internal a :: Type` this fails {{{#!hs -- • Expected kind ‘Sig Type -> Type’, -- but ‘dom’ has kind ‘Sig a -> Type’ -- • In the type ‘dom’ -- In the type instance declaration for ‘Domain’ -- In the instance declaration for ‘Syntactic (AST dom (Full a))’ -- -- • Expected a type, but ‘a1’ has kind ‘a’ -- • In the type ‘a’ -- In the type instance declaration for ‘Internal’ -- In the instance declaration for ‘Syntactic (AST dom (Full a))’ instance Syntactic (AST dom (Full a)) where type Domain (AST dom (Full a)) = dom type Internal (AST dom (Full a)) = a }}} and I have to restrict the kind of `AST` to {{{#!hs data AST :: (Sig Type -> Type) -> (Sig Type -> Type) where }}} Boo! :) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12553#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12553: Reference kind in a type instance declaration defined in another instance declaration -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: 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): It seems to work by ''un-''associating them from `Syntactic` {{{#!hs type family Domain a :: Sig u -> Type type instance Domain (AST dom (Full a)) = dom type family Internal (a :: Type) :: k type instance Internal (AST dom (Full a)) = a }}} and `instance Syntactic (AST dom (Full a))` compiles. Is there some way to get them to compile while associated? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12553#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12553: Reference kind in a type instance declaration defined in another instance declaration -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: 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 goldfire): * keywords: => TypeInType Comment: I don't understand the code you're posting, but `Internal` looks OK to me. It should be accepted. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12553#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12553: Reference kind in a type instance declaration defined in another instance declaration -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: 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): Interesting! this works {{{#!hs class Syntactic a where type Domain a :: Sig u -> Type type Internal a :: u a :: Proxy (Domain a) b :: Proxy (Internal a) -- c :: AST (Domain a) (Full (Internal a)) }}} but for some reason the method `c` breaks it. ---- Functional dependencies solve this, but they change the API in a way that doesn't work for me: {{{#!hs class Syntactic a (dom :: Sig u -> Type) | a -> dom where type Internal a :: u desugar :: ASTF dom (Internal a) -> a sugar :: a -> ASTF dom (Internal a) instance Syntactic (AST dom (Full a)) dom where type Internal (AST dom (Full a)) = a desugar = id sugar = id }}} ---- Here is another workaround, it's not perfect (need to recover `Domain`, `Internal`) but it's a start {{{#!hs class Syntactic a where type DomainInternal a :: Type desugar :: DomainInternal a -> a sugar :: a -> DomainInternal a instance Syntactic (AST dom (Full a)) where type DomainInternal (AST dom (Full a)) = AST dom (Full a) desugar x = x sugar x = x }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12553#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12553: Reference kind in a type instance declaration defined in another instance declaration -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: 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): Richard says
but `Internal` looks OK to me. It should be accepted.
Alas Jack has posted no fewer than four different declarations of `Internal`, so I'm not sure which one(s) you think should be accepted. Jack, what kind do you WANT `Internal` to have? For example, in the one that works: {{{ type family Domain a :: Sig u -> Type type family Internal (a :: Type) :: k }}} I believe we get {{{ Domain :: forall (u :: Type). Type -> Sig u -> Type Internal :: forall (k :: Type). Type -> k }}} Now when writing them in associated form we have {{{ class Syntactic a where type Domain a :: Sig u -> Type type Internal a :: u }}} and this should not really be different. I think it shoudl be accepted. But I do have a question: should we get {{{ Domain :: Type -> forall u. Sig u -> Type or Domain :: forall u. Type -> Sig u -> Type }}} and does it matter at use sites? Richard The same question arises with class methods. Given {{{ class C a where op :: forall b. Ord b => b -> a -> a }}} do we get {{{ op :: forall a. C a => forall b. Ord b => b -> a -> a or op :: forall a b. (C a, Ord b) => b -> a -> a }}} Answer: wer get the former. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12553#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12553: Reference kind in a type instance declaration defined in another instance declaration -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: 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): Recall that type families don't really have a kind because they must always appear saturated. I'll write `~>` for a function argument that must always be provided. (In the language of my [https://github.com/goldfirere/thesis dissertation], `->` used in a kind is ''matchable'' and I will use `~>` for ''unmatchable''. Currently, unmatchable functions in types must always appear saturated. Type families are the only way to write an unmatchable function in a type.) So, with {{{ class Syntactic a where type Domain a :: Sig u -> Type type Internal a :: u }}} I would expect {{{ Domain :: forall u. Type ~> Sig u -> Type Internal :: forall u. Type ~> u }}} Having the `forall` out front does matter, because it means the type family can branch on the choice of `u`. (It should really be a `pi`. And be unmatchable.) If Jack wants things to be different, then he can specify {{{ class Syntactic' a where type Domain' a :: forall u. Sig u -> Type type Internal' a :: forall u. u }}} yielding {{{ Domain' :: Type ~> forall u. Sig u -> Type Internal' :: Type -> forall u. u }}} These `forall`s describe arguments that ''cannot'' be matched against in the type family instances and so are seemingly less useful. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12553#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12553: Reference kind in a type instance declaration defined in another instance declaration -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: 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'll start out by saying that I seem to be missing something! == Example that failed in original question == It can be solved by specifying the kind of `a :: Type`: {{{#!hs -- Compiles fine! class Syntactic (a :: Type) where type Domain a :: Sig u -> Type type Internal a :: u desugar :: a -> ASTF (Domain a) (Internal a) sugar :: ASTF (Domain a) (Internal a) -> a }}} I believe this to be a bug. == I don't know what I'm doing == Replying to [comment:6 simonpj]:
Alas Jack has posted no fewer than four different declarations of `Internal`, so I'm not sure which one(s) you think should be accepted.
My bad
Jack, what kind do you WANT `Internal` to have?
None, possibly! It seems that the kind `u` is an existential kind(?) so maybe I should use `DomainInternal` directly, rather than going from `a` → `Domain, Internal` → `ASTF (Domain a) (Internal a)`... Or define an existential data type that can be converted to `ASTF _ _`. {{{#!hs data EXISTS where EX :: (Sig u -> Type) -> u -> EXISTS type family ASTify (ex :: EXISTS) :: Type where ASTify (EX dom a) = ASTF dom a }}} Both of these make certain definitions very awkward though, but figuring this out is beyond the scope of this ticket.. you go from a neat definition like: {{{#!hs instance Syntactic (a -> b) where type Domain (a -> b) = Domain a type Internal (a -> b) = Internal a -> Internal b }}} to something like this (I believe) {{{#!hs type family DomainInternalArr a b where DomainInternalArr (ASTF dom a) (ASTF dom b) = ASTF dom (a -> b) instance Syntactic (a -> b) where type DomainInternal (a -> b) = DomainInternalArr (DomainInternal a) (DomainInternal b) }}} == Non-solution == Something like this could work if #11962 gets fixed, maybe {{{#!hs class Syntactic (a :: Type) where type SyntKind a :: Type type Domain a :: Sig (SyntKind a) -> Type type Internal a :: SyntKind a }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12553#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12553: Reference kind in a type instance declaration defined in another instance declaration -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: 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): I think the following clarifying comment might help: When declaring a type family like {{{ type family F a :: u }}} the result kind `u` is actually a ''parameter'' to `F`. This type family is the same as {{{ type family G u a :: u }}} except that in `F`, the `u` is invisible. So there are no existential kinds involved. Does this help? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12553#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12553: Reference kind in a type instance declaration defined in another instance declaration -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: worksforme | 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 goldfire): * status: new => closed * resolution: => worksforme Comment: The program below, taken from the original ticket description, compiles on HEAD and 8.2.1: {{{#!hs {-# LANGUAGE PolyKinds, DataKinds, TypeFamilies #-} module Bug where import Data.Kind data Sig a = Full a | a :-> Sig a data AST :: (Sig a -> Type) -> (Sig a -> Type) -- ASTF :: (Sig a -> Type) -> (a -> Type) type ASTF dom a = AST dom (Full a) class Syntactic a where type Domain a :: Sig u -> Type type Internal a :: u desugar :: a -> ASTF (Domain a) (Internal a) sugar :: ASTF (Domain a) (Internal a) -> a }}} There's been a lot of other chatter on this ticket, but if there is still an issue here, please open a new ticket. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12553#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12553: Reference kind in a type instance declaration defined in another instance declaration -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: worksforme | 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): Replying to [comment:9 goldfire]:
.. result kind `u` is actually a ''parameter'' to `F`.
This clarified a lot. Thanks for the feedback, it works for me now -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12553#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC