Descargo de responsabilidad

Los GADT y DataKinds son un territorio inexplorado para mí, por lo que algunas de sus limitaciones y capacidades son desconocidas para mí.

La pregunta

Así que estoy escribiendo un AST para un emisor de código JavaScript, e identifiqué un caso límite entre expresiones y es que pueden ser una referencia o no. Así que he usado GADTS y datakinds para escribir este aspecto de la semántica de expresiones de JavaScript. El ast se parece a esto.

Subconjunto de la expresión AST

-- at the moment I'm just using a bool to identify if the expression 
-- behaves as an reference, but I'll probably change it due to the fact
-- a bool is pretty vague

data JSExp :: Bool -> * where

  JSNumber :: Double -> JSExp False
  JSBool :: Bool -> JSExp False

  JSReference :: Text -> JSExp True
  JSProperty :: JSExp a -> Text -> JSExp True
  JSAssign :: JSExp True -> JSExp b -> JSExp b

Esto se ve muy bien, porque una expresión de asignación requiere que la primera expresión sea una referencia como una expresión de propiedad ("test".shadyProperty) o una referencia / identificador.

El problema

Ahora quiero agregar una expresión literal de matriz, en JavaScript no debería importar lo que está en esta lista, por lo que listas como esta son legales

[a, 1, true, a.b]

Sin embargo, en mi AST esto no es legal porque hay varios tipos en la lista

data JSExp :: Bool -> * where

  -- ...

  JSArray :: [JSExp ???] -> JSExp False

let aref = JSReference "a"
in  JSArray [aref, JSNumber 2, JSBool True, JSProp aref "b"] 

Lo que va en lugar de??? para el tipo? Un problema similar ocurre cuando quiero construir un constructor para JSObject's y JSFunctionCall's, ya que estas también son expresiones.

La alma de Idris

En idris??? se vería algo así

data JSExp : Bool -> Type where

  JSArray : List (JSExp _) -> JSExp False
  JSNumber : Float -> JSExp False
  JSBool : Bool -> JSExp False

  -- ...

Almas potencialesTipo de envoltura

Una alma que no es como la Idris, tendría un tipo de envoltura como esta

data JSExpWrap = Refs (JSExp True) | NoRef (JSExp False)

Esto haría que la API de mi biblioteca sea asquerosa y no es lo que estoy buscando.

En resumen

Estoy buscando el equivalente que se encuentra en Idris, y una explicación de las implicaciones de la solución. Si no hay un equivalente, lo que estoy buscando es una solución de la siguiente mejor opción.