Problem with default signatures
Nicolas Frisby
nicolas.frisby at gmail.com
Thu Aug 23 23:21:16 CEST 2012
I've investigated this behavior a bit, and I have two things worth mentioning.
(1) One of the ingredients in this behavior is the non-injectivity
of type families. If we make the class parameter f accessible in the
signature of emptyAlt, there are no more type errors. For example, if
you can change the signature to emptyAlt :: Proxy f -> Exp (AltGRep f)
where
data Proxy (f :: * -> *) = Proxy
(Even if your code had been type checking, you would have found that
emptyAlt would be impossible to use with the signature you gave it —
its type must include at least one occurrence of each class parameter
that isn't inside an argument to a type family. That's what I mean by
"accessible", and its what the dummy parameter "Proxy f" gives us.)
Jeroen Weijers, I think this will be enough for you to get past these
errors. Please let me know if not.
The rest of this email is probably more for GHC hackers.
(2) The note [Default methods in instances] in TcInstDcls handles
GHC ticket #1061. The key idea is that a default method (those without
special signatures) intuitively results in a method definition in the
instances that rely on the default is a simple equality "method =
default_RHS". #1061 shows a situation in which this won't do; we need
the RHS to be eta-expanded with respect to the class type parameters.
But looking in TcInstDcls.tcInstanceMethods and
TcClassDcl.mkGenericDefMethBind, it seems that generic default
signatures don't do this eta-expansion.
Adding the Proxy parameter as in (1) avoids the type errors and also
seems like it's going to be necessary, so I'm not sure (2) is entirely
relevant. But I'm not seeing why generic default methods would be any
different with respect to #1061 than vanilla default methods. Perhaps
the example in #1061 could be enriched with a default signature to see
if its fix should be applied to generic default methods as well?
Lastly, regarding (1), would it make sense to throw an error when a
polymorphic signature has "inaccessible" type variables? Are these
ever useful? Maybe just a warning?
HTH
On Tue, Aug 21, 2012 at 4:45 AM, Jeroen Weijers <jeroenweijers at gmail.com> wrote:
> Hello,
>
> I am trying to create some code involving type families and default signatures. I am getting a type error that I do not understand (as far as I can see the error is wrong).
>
> I removed all code that doesn't contribute to the error:
>
>> {-# LANGUAGE DeriveGeneric, UndecidableInstances, DefaultSignatures, TypeOperators, GADTs, FlexibleContexts, TypeFamilies, FlexibleInstances #-}
>> module Database.DSH.Problem where
>>
>> import GHC.Generics
>>
>> data Exp a where
>> UnitE :: Exp ()
>> ListE :: [Exp a] -> Exp [Exp a]
>>
>> class GenericQA f where
>> type GRep f
>> type AltGRep f
>> type AltGRep f = [Exp (GRep f)]
>> gToExp :: f a -> Exp (GRep f)
>> emptyAlt :: Exp (AltGRep f)
>> default emptyAlt :: (AltGRep f ~ [Exp (GRep f)]) => Exp (AltGRep f)
>> emptyAlt = ListE []
>>
>> instance GenericQA U1 where
>> type GRep U1 = ()
>> gToExp U1 = UnitE
>
>
> This gives me the following type errors:
>
>> Problem.hs:19:10:
>> Couldn't match type `AltGRep f0' with `[Exp ()]'
>> Expected type: AltGRep U1
>> Actual type: AltGRep f0
>> Expected type: Exp (AltGRep U1)
>> Actual type: Exp (AltGRep f0)
>> In the expression: (Database.DSH.Problem.$gdmemptyAlt)
>> In an equation for `emptyAlt':
>> emptyAlt = (Database.DSH.Problem.$gdmemptyAlt)
>>
>> Problem.hs:19:10:
>> Couldn't match type `GRep f0' with `()'
>> Expected type: [Exp (GRep f0)]
>> Actual type: AltGRep f0
>> In the expression: (Database.DSH.Problem.$gdmemptyAlt)
>> In an equation for `emptyAlt':
>> emptyAlt = (Database.DSH.Problem.$gdmemptyAlt)
>> In the instance declaration for `GenericQA U1'
>
> In this error the type variable f0 is mentioned but as far as I understand it f should have been instantiated to U1 and not to a variable f0. I've tried many variations on the default type signature for emptyAlt but haven't found any that doesn't result in this error. Can somebody explain what is going wrong here?
>
> Cheers,
>
> Jeroen
> _______________________________________________
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users at haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
More information about the Glasgow-haskell-users
mailing list