Opened 3 years ago

Last modified 3 years ago

#12551 new feature request

Make type indices take local constraints into account in type instance declaration

Reported by: Iceland_jack Owned by: Iceland_jack
Priority: normal Milestone:
Component: Compiler Version: 8.0.1
Keywords: TypeFamilies Cc:
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 (last modified by Iceland_jack)

Given

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)):

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 ‘constraint’ trick (link) but I cannot use the Rep instance as before:

--     • 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

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

Change History (7)

comment:1 Changed 3 years ago by Iceland_jack

Simplified example

infixr :->
data Sig x where
  Full  :: a          -> Sig a
  (:->) :: a -> Sig a -> 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

instance a' ~ Full a => Syntactic (Exp a') where
  type Rep (Exp (Full a)) = a

and/or

instance a' ~ Full a => Syntactic (Exp a') where
  type Rep (Exp a') = a

and/or

instance a' ~ Full a => Syntactic (Exp a') where
  type Rep (Exp _) = a
Last edited 3 years ago by Iceland_jack (previous) (diff)

comment:2 in reply to:  description Changed 3 years ago by Iceland_jack

Description: modified (diff)
Last edited 3 years ago by Iceland_jack (previous) (diff)

comment:3 Changed 3 years ago 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.

comment:4 Changed 3 years ago by Iceland_jack

I vaguely remember that discussion. That's fine, I will add the workaround.

Could this be mentioned in the error message?

comment:5 Changed 3 years ago by goldfire

Yes, I think it should. Might you add it? :)

comment:7 Changed 3 years ago by Iceland_jack

Owner: set to Iceland_jack
Note: See TracTickets for help on using tickets.