sheas.hs

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE PolyKinds #-}

import Data.Kind (Type)
import GHC.TypeLits (Nat)

class HasAssociatedKind k where
  type AssociatedKind k :: k'
instance HasAssociatedKind Type where
  type AssociatedKind Type = Type
instance HasAssociatedKind k2 => HasAssociatedKind (k1 -> k2) where
  type AssociatedKind (k1 -> k2) = AssociatedKind k2

class (HasAssociatedKind k, AssociatedKind k ~ Type) => UseAssociatedKind (t :: k) where
  type AssociatedType t x :: Type
instance (HasAssociatedKind k, AssociatedKind k ~ Type) => UseAssociatedKind (t :: k) where
  type AssociatedType t x = x

a :: UseAssociatedKind Int => AssociatedType Int ()
a = ()

b :: UseAssociatedKind Maybe => AssociatedType Maybe ()
b = ()

-- `c` fails to compile with an horrible message about AllowAmbiguousTypes
c :: forall (t :: Type -> Nat). UseAssociatedKind t => AssociatedType t ()
c = ()

d :: forall (t :: Nat -> Type ). UseAssociatedKind t => AssociatedType t ()
d = ()