bug.hs

{-# LANGUAGE TypeFamilies, DataKinds, TypeOperators, FlexibleContexts, ScopedTypeVariables, GADTs,
    FlexibleInstances, UndecidableInstances #-}

{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}

import GHC.TypeLits
import Data.Proxy

data Natty :: Nat -> * where
  Zy :: Natty 0
  Sy :: Natty n -> Natty (1 + n)

toInt :: forall n. Natty n -> Int
toInt n = toInt' n 0
  where toInt' :: forall n. Natty n -> Int -> Int
        toInt' Zy    acc = acc
        toInt' (Sy p) acc = toInt' p (acc+1)

instance Show (Natty n) where
  show = show . toInt

class ToNatty (n :: Nat) where
  type NattyType n
  getNatty :: Proxy n -> NattyType n

instance ToNatty 0 where
  type NattyType 0 = Natty 0
  getNatty _ = Zy

instance (ToNatty (n-1)) => ToNatty n where
  type NattyType n = Natty n
  getNatty _ = Sy (getNatty (Proxy :: Proxy (n-1)))

main :: IO ()
-- Overlapping instances for ToNatty 0
--   arising from a use of ‘getNatty’
-- Matching instances:
--   instance ToNatty 0 -- Defined at bug.hs:26:10
--   instance ToNatty (n - 1) => ToNatty n -- Defined at bug.hs:30:10
-- In the second argument of ‘($)’, namely
--   ‘getNatty (Proxy :: Proxy 12)’
-- In the expression: print $ getNatty (Proxy :: Proxy 12)
-- In an equation for ‘main’:
--     main = print $ getNatty (Proxy :: Proxy 12)
main = print $ getNatty (Proxy :: Proxy 12)