Poly-kinded type family
alice
alicekoroleva239 at gmail.com
Mon Apr 30 12:27:57 UTC 2018
Hello. I’m trying to make a type family with resolving it inside type checking classes, like CmpNat. Its type signature is «type family Cmp (a :: k1) (b :: k2) :: Ordering», so the function is poly kinded. But it seems unclear how to make its TyCon. I’ve tried to follow the CmpNat and CmpSymbol style, and also saw Any TyCon in TysWiredIn. So this is my attempt:
typeCmpTyCon :: TyCon
typeCmpTyCon =
mkFamilyTyCon name
(binders ++ (mkTemplateAnonTyConBinders [ input_kind1, input_kind2 ]))
orderingKind
Nothing
(BuiltInSynFamTyCon ops)
Nothing
NotInjective
where
name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "Cmp")
typeCmpTyFamNameKey typeCmpTyCon
ops = BuiltInSynFamily
{ sfMatchFam = matchFamCmpType
, sfInteractTop = interactTopCmpType
, sfInteractInert = \_ _ _ _ -> []
}
binders@[kv1, kv2] = mkTemplateKindTyConBinders [ liftedTypeKind, liftedTypeKind ]
input_kind1 = mkTyVarTy (binderVar kv1)
input_kind2 = mkTyVarTy (binderVar kv2)
ghci says this:
:kind Cmp
Cmp :: forall {k0} {k1}. k0 -> k1 -> Ordering
But then I try to apply it to some values and get this exception:
:kind! Cmp 4 5
<interactive>:1:15: error:
• Expected kind ‘k0’, but ‘4’ has kind ‘Nat’
• In the first argument of ‘Cmp’, namely ‘4’
In the type ‘Cmp 4 5’
<interactive>:1:17: error:
• Expected kind ‘k1’, but ‘5’ has kind ‘Nat’
• In the second argument of ‘Cmp’, namely ‘5’
In the type ‘Cmp 4 5’
Does anyone know where I made a mistake? Any help would be appreciated.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20180430/3cf311ed/attachment.html>
More information about the ghc-devs
mailing list