Opened 15 months ago

Closed 3 months ago

Last modified 3 months ago

#12553 closed bug (worksforme)

Reference kind in a type instance declaration defined in another instance declaration

Reported by: Iceland_jack Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.0.1
Keywords: TypeInType 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)

Old code:

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

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:

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

  type Domain   a :: forall k. Sig k -> Type

Edit: This doesn't work.

Change History (11)

comment:1 Changed 15 months ago by Iceland_jack

Description: modified (diff)

comment:2 Changed 15 months ago by Iceland_jack

If I constrain the types Domain a :: Sig Type -> Type, Internal a :: Type this fails

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

data AST :: (Sig Type -> Type) -> (Sig Type -> Type) where

Boo! :)

comment:3 Changed 15 months ago by Iceland_jack

It seems to work by un-associating them from Syntactic

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?

comment:4 Changed 15 months ago by goldfire

Keywords: TypeInType added

I don't understand the code you're posting, but Internal looks OK to me. It should be accepted.

comment:5 Changed 15 months ago by Iceland_jack

Interesting! this works

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:

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

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

comment:6 Changed 15 months ago 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.

comment:7 Changed 15 months ago 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 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 foralls describe arguments that cannot be matched against in the type family instances and so are seemingly less useful.

comment:8 in reply to:  6 Changed 15 months ago 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 but this is not the right solution:

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

-- Does NOT compile
-- instance Syntactic (ASTF dom a) where
--   type Domain   (ASTF dom a) = dom
--   type Internal (ASTF dom a) = a
--   desugar x = x
--   sugar   x = x

I believe this to be a bug.

I don't know what I'm doing

Replying to 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 aDomain, InternalASTF (Domain a) (Internal a)... Or define an existential data type that can be converted to ASTF _ _.

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:

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)

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)

The inelegance indicates that this is the wrong choice.

Non-solution

Something like this could work if #11962 gets fixed, maybe

class Syntactic (a :: Type) where
  type SyntKind a :: Type

  type Domain   a :: Sig (SyntKind a) -> Type
  type Internal a :: SyntKind a
Last edited 15 months ago by Iceland_jack (previous) (diff)

comment:9 Changed 15 months ago 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?

comment:10 Changed 3 months ago by goldfire

Resolution: worksforme
Status: newclosed

The program below, taken from the original ticket description, compiles on HEAD and 8.2.1:

{-# 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.

comment:11 in reply to:  9 Changed 3 months ago by Iceland_jack

Replying to goldfire:

.. result kind u is actually a parameter to F.

This clarified a lot. Thanks for the feedback, it works for me now

Note: See TracTickets for help on using tickets.