
Hi, Am Dienstag, den 01.05.2018, 22:05 -0400 schrieb Richard Eisenberg:
We can boil it down to one rule for these situations: RULE. Braces used in type declarations affect only the types of terms declared within the declaration. The braces have no effect whatsoever on the kind of the type(s) declared.
With this in mind, I'll answer the questions below:
On May 1, 2018, at 12:56 PM, Iavor Diatchki
wrote: -- 1) The "normal" case. I've written the types of the introduces names underneath, are they correct? data T1 {k} (a :: k) = C1 -- T1 :: forall {k::Type}. k -> Type -- C1 :: forall {k::Type} (a :: k). T1 {k} a
I would say we get
T1 :: forall (k :: Type) -> k -> Type -- T1 has *2* visible arguments C1 :: forall {k :: Type} (a :: k). T1 k a -- C1 has one inferred and one specified type argument
I think this is highly confusing. The {k} is on T1, but it does not affect T1, but rather something else? What is wrong with “if you want to have different specificity on the tycon and the datacon, use GADTSyntax”? Cheers, Joachim -- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/