Come utilizzare il confronto in GHC.TypeLits

Question

Ho riscontrato problemi con GHC.TypeLits. Si consideri il seguente GADT:

data Foo :: Nat -> * where 
    SmallFoo :: (n <= 2) => Foo n 
    BigFoo :: (3 <= n) => Foo n 

La mia comprensione è che ora ogni n, il tipo Foo n è popolato da esattamente un valore (ovvero uno SmallFoo o un BigFoo a seconda del valore della n).

Ma se ora voglio costruire un esempio concreto come segue:

myFoo :: Foo 4 
myFoo = BigFoo 

Poi GHC (7.6.2) sputa fuori il seguente messaggio di errore:

No instance for (3 <= 4) arising from a use of `BigFoo' 
Possible fix: add an instance declaration for (3 <= 4) 
In the expression: BigFoo 
In an equation for `myFoo': myFoo = BigFoo 

Questo sembra strano - I ci si aspetta che ci sia un'istanza predefinita per tali confronti di livello di tipo nat. Come posso esprimere questo tipo di vincoli nel mio costruttore di dati utilizzando i tipi di livello naturali?

Answer 1

Il Risolutore per TypeLists non è in GHC al momento, secondo lo status page ci sono alcune possibilità che sarà in GHC 7.8 ad ottobre o qualcosa del genere.

Forse è meglio usare other packages per ora.

Answer 2

Questo compila sull'attuale capo del ramo type-nats, che dovrebbe (si spera) essere unito per 7.8.

{-# LANGUAGE DataKinds #-} 
{-# LANGUAGE FlexibleContexts #-} 
{-# LANGUAGE GADTs #-} 
{-# LANGUAGE KindSignatures #-} 
{-# LANGUAGE TypeOperators #-} 

module X where 

import GHC.TypeLits 

data Foo :: Nat -> * where 
    SmallFoo :: (n <= 2) => Foo n 
    BigFoo :: (3 <= n) => Foo n 

myFoo :: Foo 4 
myFoo = BigFoo 

Dove se myFoo viene modificata per essere di tipo Foo 1 non riesce a compilare, presumibilmente perché il vincolo x <= y classe è espanso al vincolo (x <=? y) ~ 'True uguaglianza:

$ /Source/ghc/inplace/bin/ghc-stage1 /tmp/blah.hs 
[1 of 1] Compiling X    (/tmp/blah.hs, /tmp/blah.o) 

/tmp/blah.hs:16:13: 
    Couldn't match type ‛3 <=? 1’ with ‛'True’ 
    In the expression: BigFoo 
    In an equation for ‛myFoo’: myFoo = BigFoo