TypeNats ghc vs mhs differences

[claudeha]

{-# LANGUAGE DataKinds #-}                         
 -- pragma needed for ghc-9.12.2
module TypeNat where                           
   
import GHC.TypeLits (Nat)                        
   -- import needed for kind signature in ghc-9.12.2   
  -- also in GHC.TypeNats                                       
  -- import fails in mhs-0.15.5.0
  -- import not needed in mhs-0.15.5.0            

data Foo (a :: Nat) = Foo                          
 -- kind signature not needed for ghc-9.12.2
  -- kind signature needed in mhs-0.15.5.0
  deriving (Show)                                 

main = print (Foo :: Foo 665)
  -- without kind signature mhs fails to unify Nat with Type
  -- without import ghc doesn't find Nat

I could use CPP to make the import conditional or add a module for impl mhs that fakes enough of GHC.TypeLits, so its not really a blocker at the moment

[augustss]

I'll add GHC.TypeLits to the ghc-compat package.

[claudeha]

MicroHs seems to be missing a way to do something like

withNat :: Integer -> (forall (n :: Nat) . KnownNat n => Proxy n -> r) -> r

GHC does something with SNat that I haven't fully understood yet.

[augustss]

I'll have to implement something like GHC.Magic.withDictto be able to do withNat. I've not done that yet.