[GHC] #12551: Make type indices take local constraints into account in type instance declaration
#12551: Make type indices take local constraints into account in type instance declaration -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature | Status: new request | Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Keywords: TypeFamilies | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Given {{{#!hs infixl 1 :$ infixr :-> data Sig x where Full :: a -> Sig a (:->) :: a -> b -> Sig a data AST dom a where Sym :: dom a -> AST dom a (:$) :: AST dom (a:->b) -> AST dom (Full a) -> AST dom b class Syntactic a dom | a -> dom where type Rep a desugar :: a -> AST dom (Full (Rep a)) sugar :: AST dom (Full (Rep a)) -> a }}} I want to be able to define the trivial instance for `Syntactic (AST dom (Full a))`: {{{#!hs instance Syntactic (AST dom (Full a)) dom where type Rep (AST dom (Full a)) = a desugar, sugar :: AST dom (Full a) -> AST dom (Full a) desugar = id sugar = id }}} This should be the only `Syntactic` instance for `AST _ _` so I would like to apply the [http://chrisdone.com/posts/haskell-constraint-trick ‘constraint’ trick] ([https://gist.github.com/Icelandjack/5afdaa32f41adf3204ef9025d9da2a70 #blog-reddit-constraint-trick-for-instances link]) but I cannot use the `Rep` instance as before: {{{#!hs -- • Type indexes must match class instance head -- Found ‘AST dom ('Full a)’ but expected ‘AST dom full_a’ -- • In the type instance declaration for ‘Rep’ -- In the instance declaration for ‘Syntactic (AST dom full_a) dom’ instance full_a ~ Full a => Syntactic (AST dom full_a) dom where type Rep (AST dom (Full a)) = a }}} Maybe this could be accepted, given that `full_a ~ Full a`, therefore the instance head is equal to `AST dom (Full a)`? My current workaround is using a type family {{{#!hs type family Edrú a where Edrú (Full a) = a instance full_a ~ Full a => Syntactic (AST dom full_a) dom where type Rep (AST dom full_a) = Edrú full_a desugar, sugar :: AST dom (Full a) -> AST dom (Full a) desugar = id sugar = id }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12551 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12551: Make type indices take local constraints into account in type instance declaration -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: TypeFamilies 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): Simplified example {{{#!hs infixr :-> data Sig x where Full :: a -> Sig a (:->) :: a -> b -> Sig a data Exp a where Lit :: Int -> Exp (Full Int) Add :: Exp (Int :-> Int :-> Full Int) class Syntactic a where type Rep a desugar :: a -> Exp (Full (Rep a)) sugar :: Exp (Full (Rep a)) -> a instance Syntactic (Exp (Full a)) where type Rep (Exp (Full a)) = a desugar, sugar :: Exp (Full a) -> Exp (Full a) desugar = id sugar = id }}} ---- I would like this to compile {{{#!hs instance a' ~ Full a => Syntactic (Exp a') where type Rep (Exp (Full a)) = a }}} and/or {{{#!hs instance a' ~ Full a => Syntactic (Exp a') where type Rep (Exp a') = a }}} and/or {{{#!hs instance a' ~ Full a => Syntactic (Exp a') where type Rep (Exp _) = a }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12551#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
Given
{{{#!hs infixl 1 :$ infixr :-> data Sig x where Full :: a -> Sig a (:->) :: a -> b -> Sig a
data AST dom a where Sym :: dom a -> AST dom a (:$) :: AST dom (a:->b) -> AST dom (Full a) -> AST dom b
class Syntactic a dom | a -> dom where type Rep a desugar :: a -> AST dom (Full (Rep a)) sugar :: AST dom (Full (Rep a)) -> a }}}
I want to be able to define the trivial instance for `Syntactic (AST dom (Full a))`:
{{{#!hs instance Syntactic (AST dom (Full a)) dom where type Rep (AST dom (Full a)) = a desugar, sugar :: AST dom (Full a) -> AST dom (Full a) desugar = id sugar = id }}}
This should be the only `Syntactic` instance for `AST _ _` so I would
#12551: Make type indices take local constraints into account in type instance declaration -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- @@ -7,2 +7,2 @@ - Full :: a -> Sig a - (:->) :: a -> b -> Sig a + Full :: a -> Sig a + (:->) :: a -> Sig a -> Sig a New description: Given {{{#!hs infixl 1 :$ infixr :-> data Sig x where Full :: a -> Sig a (:->) :: a -> Sig a -> Sig a data AST dom a where Sym :: dom a -> AST dom a (:$) :: AST dom (a:->b) -> AST dom (Full a) -> AST dom b class Syntactic a dom | a -> dom where type Rep a desugar :: a -> AST dom (Full (Rep a)) sugar :: AST dom (Full (Rep a)) -> a }}} I want to be able to define the trivial instance for `Syntactic (AST dom (Full a))`: {{{#!hs instance Syntactic (AST dom (Full a)) dom where type Rep (AST dom (Full a)) = a desugar, sugar :: AST dom (Full a) -> AST dom (Full a) desugar = id sugar = id }}} This should be the only `Syntactic` instance for `AST _ _` so I would like to apply the [http://chrisdone.com/posts/haskell-constraint-trick ‘constraint’ trick] ([https://gist.github.com/Icelandjack/5afdaa32f41adf3204ef9025d9da2a70 #blog-reddit-constraint-trick-for-instances link]) but I cannot use the `Rep` instance as before: {{{#!hs -- • Type indexes must match class instance head -- Found ‘AST dom ('Full a)’ but expected ‘AST dom full_a’ -- • In the type instance declaration for ‘Rep’ -- In the instance declaration for ‘Syntactic (AST dom full_a) dom’ instance full_a ~ Full a => Syntactic (AST dom full_a) dom where type Rep (AST dom (Full a)) = a }}} Maybe this could be accepted, given that `full_a ~ Full a`, therefore the instance head is equal to `AST dom (Full a)`? My current workaround is using a type family {{{#!hs type family Edrú a where Edrú (Full a) = a instance full_a ~ Full a => Syntactic (AST dom full_a) dom where type Rep (AST dom full_a) = Edrú full_a desugar, sugar :: AST dom (Full a) -> AST dom (Full a) desugar = id sugar = id }}} -- Comment (by Iceland_jack): Replying to [ticket:12551 Iceland_jack]: like to apply the [http://chrisdone.com/posts/haskell-constraint-trick ‘constraint’ trick] ([https://gist.github.com/Icelandjack/5afdaa32f41adf3204ef9025d9da2a70 #blog-reddit-constraint-trick-for-instances link]) but I cannot use the `Rep` instance as before:
{{{#!hs -- • Type indexes must match class instance head -- Found ‘AST dom ('Full a)’ but expected ‘AST dom full_a’ -- • In the type instance declaration for ‘Rep’ -- In the instance declaration for ‘Syntactic (AST dom full_a)
dom’
instance full_a ~ Full a => Syntactic (AST dom full_a) dom where type Rep (AST dom (Full a)) = a }}}
Maybe this could be accepted, given that `full_a ~ Full a`, therefore
the instance head is equal to `AST dom (Full a)`?
My current workaround is using a type family
{{{#!hs type family Edrú a where Edrú (Full a) = a
instance full_a ~ Full a => Syntactic (AST dom full_a) dom where type Rep (AST dom full_a) = Edrú full_a desugar, sugar :: AST dom (Full a) -> AST dom (Full a) desugar = id sugar = id }}}
-- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12551#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12551: Make type indices take local constraints into account in type instance declaration -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: TypeFamilies 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): What you wish to do was possible previously (7.8? 7.6?) but it caused quite a bit of complication in processing associated type instances. Simon proposed restricting the syntax of associated type instances to require that the instances be defined over precisely the types in the head of the class instance. No one objected. So he made the change. Your "workaround" is precisely the way to do what you want. It is a bit frustrating in this particular case, where what you want is "obviously" correct, but I don't quite think it's worth restoring the old, complicated implementation of associated types here. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12551#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12551: Make type indices take local constraints into account in type instance declaration -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: TypeFamilies 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 vaguely remember that discussion. That's fine, I will add the [https://gist.github.com/Icelandjack/5afdaa32f41adf3204ef9025d9da2a70#workaro... workaround]. Could this be mentioned in the error message? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12551#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12551: Make type indices take local constraints into account in type instance declaration -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: TypeFamilies 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): Yes, I think it should. Might you add it? :) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12551#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12551: Make type indices take local constraints into account in type instance declaration -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: TypeFamilies 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): [https://www.youtube.com/watch?v=BD4nUQZaGNc What do I look like, a guy who's not lazy?] ---- I will :D -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12551#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12551: Make type indices take local constraints into account in type instance declaration -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Iceland_jack Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: TypeFamilies 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 Iceland_jack): * owner: => Iceland_jack -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12551#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC