On 07/06/2015 07:29 PM, Silvio Frischknecht wrote:
looks like the problem are the 'e's. you can see it from
Could not deduce (TFunOut t1 e ~ TFunOut t1 e0)
the e0 comes from the output of TFunIn/TFunOut and the instance does not know that it is the same as the e variable you use.
I don't know exactly what your program does. but if e is just a phantom/security parameter you can do it like this.
type family TFunIn t :: * -> *
type instance TFunIn IdT = Signal
type instance TFunIn (ComposeT t1 t2) = TFunIn t2
instance (SignalT t1 e, SignalT t2 e, TFunOut t2 ~ TFunIn t1) => SignalT (ComposeT t1 t2) e where transform _ x = (transform (undefined :: t1) . transform (undefined :: t2)) x
Otherwise you will have to find a way to prove that the 'e's are the same
Cheers Silvio
Hi Silvio, The `e` type is important. The problem with not including `e` in the `TFunIn` is that I will want to define: type instance TFunIn DoubleT e = (Signal e, Signal e) which I cannot express without specifying the `e` type parameter. And it cannot be a closed type family. So what can I prove that the `e`s are the same? The intuition I get from the instance declaration is that "they/it" are the same: instance (SignalT t1 e, SignalT t2 e, TFunOut t2 e ~ TFunIn t1 e) => SignalT (ComposeT t1 t2) e where transform _ x = (transform (undefined :: t1) . transform (undefined :: t2)) x Thanks. -- Leza Morais Lutonda, Lemol-C http://lemol.github.io 50 Aniversario de la Cujae. Inaugurada por Fidel el 2 de diciembre de 1964 http://cujae.edu.cu