MaybeBug.hs

{-# LANGUAGE DataKinds
           , ScopedTypeVariables
           , TypeApplications
           , TypeFamilies
           , PolyKinds
           , StandaloneKindSignatures
           #-}

module MaybeBug where

type family Undefined where

data Relation n m = MkR

type Fam :: forall a b c . Relation a b -> Relation b c -> Relation a c
type family Fam lt o where
  Fam @a @b @c alt MkR = Undefined -- @a @b @c are not a problem on their own

  Fam alt MkR = alt -- this is fine (but isn't (alt :: Relation a b)?)

  -- Fam @a @b @c alt MkR = alt
  -- Produces error - Why does this work without @a @b @c but not with?
  -- ANSWER: The `alt` return value makes ghc infer the invisible arguments as @a @b @b, so
  -- this equation ends up matching fewer cases than if it were @a @b @c

{-
MaybeBug.hs:21:26: error:
    • Expected kind ‘Relation a c’, but ‘alt’ has kind ‘Relation a b’
    • In the type ‘alt’
      In the type family declaration for ‘Fam’
   |
21 |   Fam @a @b @c alt MkR = alt
   |
-}