Poly-kinded type family

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
4 messages Options
Reply | Threaded
Open this post in threaded view
|

Poly-kinded type family

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

_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Poly-kinded type family

Richard Eisenberg-4
Hi Alice,

You'll need mkTemplateTyConBinders, not the two variants of that function you use below. The problem is that both mkTemplateKindTyConBinders and mkTemplateAnonTyConBinders pull Uniques starting from the same value, and so GHC gets very confused when multiple arguments to your TyCon have the same Uniques. mkTemplateTyConBinders, on the other hand, allows you to specify dependency among your arguments without confusing Uniques. You can see a usage of this function in TysPrim.proxyPrimTyCon.

I hope this helps!
Richard

PS: I've made this mistake myself several times, and it's quite baffling to debug!

On Apr 30, 2018, at 8:27 AM, alice <[hidden email]> wrote:

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.
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Poly-kinded type family

alice
Thanks a lot, this helped!

But sorry for asking, before this problem I evaluated Cmp on some values with * kinds, and I used (mkTemplateAnonTyConBinders [ liftedTypeKind, liftedTypeKind ]) to make the input kinds for TyCon.
Changing function to mkTemplateTyConBinders (right now this part looks like 'binders = mkTemplateTyConBinders [ liftedTypeKind, liftedTypeKind ] (\ks -> ks)') made my type family not evaluating:

:kind! Cmp 4 5
Cmp 4 5 :: Ordering
= Cmp 4 5

And before that change:

:kind! Cmp (Proxy 5) (Proxy 4)
Cmp (Proxy 5) (Proxy 4) :: Ordering
= 'GT

I can see from debug output that before that change functions in BuiltInSynFamily like matchFamCmpType (has the same meaning as matchFamCmpNat) had been applied to values, but now they aren’t. What am I missing?

30 апр. 2018 г., в 17:38, Richard Eisenberg <[hidden email]> написал(а):

Hi Alice,

You'll need mkTemplateTyConBinders, not the two variants of that function you use below. The problem is that both mkTemplateKindTyConBinders and mkTemplateAnonTyConBinders pull Uniques starting from the same value, and so GHC gets very confused when multiple arguments to your TyCon have the same Uniques. mkTemplateTyConBinders, on the other hand, allows you to specify dependency among your arguments without confusing Uniques. You can see a usage of this function in TysPrim.proxyPrimTyCon.

I hope this helps!
Richard

PS: I've made this mistake myself several times, and it's quite baffling to debug!

On Apr 30, 2018, at 8:27 AM, alice <[hidden email]> wrote:

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.
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs



_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Poly-kinded type family

Richard Eisenberg-4
I'm afraid I don't know a quick answer to that one. Does anyone else? If no one answers, write back in a few days and I'll look into it.

Richard

On May 1, 2018, at 3:09 AM, alice <[hidden email]> wrote:

Thanks a lot, this helped!

But sorry for asking, before this problem I evaluated Cmp on some values with * kinds, and I used (mkTemplateAnonTyConBinders [ liftedTypeKind, liftedTypeKind ]) to make the input kinds for TyCon.
Changing function to mkTemplateTyConBinders (right now this part looks like 'binders = mkTemplateTyConBinders [ liftedTypeKind, liftedTypeKind ] (\ks -> ks)') made my type family not evaluating:

:kind! Cmp 4 5
Cmp 4 5 :: Ordering
= Cmp 4 5

And before that change:

:kind! Cmp (Proxy 5) (Proxy 4)
Cmp (Proxy 5) (Proxy 4) :: Ordering
= 'GT

I can see from debug output that before that change functions in BuiltInSynFamily like matchFamCmpType (has the same meaning as matchFamCmpNat) had been applied to values, but now they aren’t. What am I missing?

30 апр. 2018 г., в 17:38, Richard Eisenberg <[hidden email]> написал(а):

Hi Alice,

You'll need mkTemplateTyConBinders, not the two variants of that function you use below. The problem is that both mkTemplateKindTyConBinders and mkTemplateAnonTyConBinders pull Uniques starting from the same value, and so GHC gets very confused when multiple arguments to your TyCon have the same Uniques. mkTemplateTyConBinders, on the other hand, allows you to specify dependency among your arguments without confusing Uniques. You can see a usage of this function in TysPrim.proxyPrimTyCon.

I hope this helps!
Richard

PS: I've made this mistake myself several times, and it's quite baffling to debug!

On Apr 30, 2018, at 8:27 AM, alice <[hidden email]> wrote:

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.
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs




_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs