assertion failure (in incorrect code)

[sweirich]

Prelude> :r [1 of 1] Compiling Singletons ( singletons.hs, interpreted ) *\ Exception: ASSERT failed! file compiler/typecheck/TcCanonical.hs, line 1093

{-# LANGUAGE GADTs, PolyKinds, TypeOperators, TemplateHaskell,
             DataKinds, TypeFamilies, UndecidableInstances,
             FlexibleContexts, RankNTypes, ScopedTypeVariables,
             FlexibleInstances #-}
{-# OPTIONS_GHC -fwarn-unticked-promoted-constructors #-}

module Singletons where

-- A version of singletons designed to work with kind equalities
-- and with typelits

import Data.Type.Equality
import GHC.Exts
import Data.Type.Bool
import Data.Proxy

import GHC.TypeLits
import Unsafe.Coerce

-- basic singletons stuff

data family Sing (a :: k)

class SingI (a :: k) where sing :: Sing a

class SingKind k where
  type DemoteRep k :: *
  fromSing :: Sing (x :: k) -> DemoteRep k

----------------------------------------------------------------------
---- SingInstance ----------------------------------------------------
----------------------------------------------------------------------

-- | A 'SingInstance' wraps up a 'SingI' instance for explicit handling.
data SingInstance (a :: k) where
  SingInstance :: SingI a => SingInstance a

-- dirty implementation of explicit-to-implicit conversion
newtype DI a = Don'tInstantiate (SingI a => SingInstance a)

-- | Get an implicit singleton (a 'SingI' instance) from an explicit one.
singInstance :: forall (a :: k). Sing a -> SingInstance a
singInstance s = with_sing_i SingInstance
  where
    with_sing_i :: (SingI a => SingInstance a) -> SingInstance a
    with_sing_i si = unsafeCoerce (Don'tInstantiate si) s

withSingI :: Sing n -> (SingI n => r) -> r
withSingI sn r =
  case singInstance sn of
    SingInstance -> r

----------------------------------------------------------------------
-- singletons and type-lit natural numbers 
----------------------------------------------------------------------

data instance Sing (n :: Nat) = KnownNat n => SNat

instance KnownNat n => SingI n where sing = SNat

instance SingKind Nat where
  type DemoteRep Nat = Integer
  fromSing (SNat :: Sing n) = natVal (Proxy :: Proxy n)

sEqNat :: forall a b. Sing a -> Sing b -> Maybe (a :~: b)
sEqNat s1 s2 = 
  withSingI s1 $ withSingI s2 $ sameNat (Proxy :: Proxy a) (Proxy :: Proxy b)

[sweirich]

The code is not type correct because I was confusing KnownNat and SingI constraints.