2012-09-24 12 views
5

Estoy tratando de recuperar el Symbol utilizado en el tipo de un valor:No se puede utilizar el tipo de firma ghci-inferido para la función de regresar Sing (d :: Símbolo)

{-# LANGUAGE GADTs #-} 
{-# LANGUAGE KindSignatures #-} 
{-# LANGUAGE DataKinds #-} 
{-# LANGUAGE ScopedTypeVariables #-} 
module Temp where 

import GHC.TypeLits 

data Temp (d :: Symbol) (a :: *) where 
    T :: a -> Temp d a 

{- 
description :: SingI Symbol d => Temp d a -> Sing Symbol d 
-} 
description (_ :: Temp d a) = (sing :: Sing d) 

Esto carga bien en ghci (versión 7.6.1):

% ghci 
GHCi, version 7.6.1: http://www.haskell.org/ghc/ :? for help 
Loading package ghc-prim ... linking ... done. 
Loading package integer-gmp ... linking ... done. 
Loading package base ... linking ... done. 
Prelude> :l Temp 
[1 of 1] Compiling Temp    (Temp.hs, interpreted) 
Ok, modules loaded: Temp. 
*Temp> :t description 
description :: SingI Symbol d => Temp d a -> Sing Symbol d 

Sin embargo, si trato de utilizar el tipo inferido por ghci en el propio módulo (eliminando el comentario de la línea en Temp.hs), me sale el siguiente error:

Temp.hs:14:16: 
    `SingI' is applied to too many type arguments 
    In the type signature for `description': 
     description :: SingI Symbol d => Temp d a -> Sing Symbol d 

Lo que tiene sentido para mí, ya que Sing and SingI seem to take a single parameter in the documentation.

¿Cuál es la firma de tipo adecuada para description?

+2

Parece un error en la impresora bonita; parece que no debería ser bonito: ¡imprima valores inferidos de argumentos de tipo implícito si no puede dar esos argumentos amables explícitamente! –

+1

Observé la misma pantalla con errores con 'Nat'. Supuse que estaba intentando imprimir una firma tipo de alguna manera, pero mostrar incorrectamente un argumento tipo implícito tiene más sentido ... –

Respuesta

2

Ok, lo tiene a través de algún monkeying sobre: ​​

description :: SingI d => Temp d a -> Sing d 

Parece que hay un poco de reescritura cobarde pasando, pero lo suficientemente bueno por ahora.

Cuestiones relacionadas