Opened 11 months ago
Last modified 11 months ago
#12553 new bug
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 )
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 (9)
comment:1 Changed 11 months ago by
Description: | modified (diff) |
---|
comment:2 Changed 11 months ago by
comment:3 Changed 11 months ago by
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 11 months ago by
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 11 months ago by
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 follow-up: 8 Changed 11 months ago by
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 11 months ago by
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 forall
s describe arguments that cannot be matched against in the type family instances and so are seemingly less useful.
comment:8 Changed 11 months ago by
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 a
→ Domain, Internal
→ ASTF (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
comment:9 Changed 11 months ago by
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?
If I constrain the types
Domain a :: Sig Type -> Type
,Internal a :: Type
this failsand I have to restrict the kind of
AST
toBoo! :)