Skip to content

Instantly share code, notes, and snippets.

Last active Jan 19, 2019
What would you like to do?
Another exposition of Edward's "Closed kinds aren't as closed as you'd think"
{-# language TypeApplications #-}
{-# language TypeFamilies #-}
{-# language FlexibleInstances #-}
{-# language ScopedTypeVariables #-}
data Unit = U
class C (k :: Unit) where
get :: Int
instance C 'U where
get = 0
-- this can be defined already here
standaloneGet :: forall (t :: Unit) . C t => Int
standaloneGet = get @t
-- the problematic 'matchable' type family
type family Succ :: Unit -> Unit
-- Note that this is different:
type family Succ1 (x :: Unit) :: Unit
instance C (f 'U) where
get = 1
results :: [Int]
results = [get @'U, get @(Succ 'U)]
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment