[Haskell-cafe] Possible ghc bug
Brandon Allbery
allbery.b at gmail.com
Wed Apr 10 18:16:25 UTC 2019
More precisely, given that definition and no type signature and no fundeps
or other constraints, ghci gave you the most general type for "add", which
is indeed ambiguous as there is no way for it to prove from the definition
of class Newtype that all the "b"s should be the same. This ambiguity is
why fundeps (and type families) exist: they extend the semantics of
typeclasses to allow this determination.
Without AllowAmbiguousTypes, it would have told you this because
typeclasses also prevent its resolution as part of using the "add"
function. But TypeApplications lets you specify the "hidden" types, hence
the AllowAmbiguousTypes extension for when you actually intend to use
TypeApplications that way. (It's something of a Big Hammer; it'd be nice if
it could be constrained to the specific types where you want to use that.)
On Wed, Apr 10, 2019 at 11:27 AM Sylvain Henry <sylvain at haskus.fr> wrote:
> >So the question is: How come the compiler does not accept its own type
> signature? Why had it not refused to compile even without one, and only
> upon specification of said signature did the compilation break?
>
> It is explained here:
> https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html?#extension-AllowAmbiguousTypes
>
> *> definition* of ambiguity: a type ty is ambiguous if and only if
> ((undefined :: ty) :: ty) would fail to typecheck.
>
> The type of "add" is ambiguous.
>
> Regards,
> Sylvain
>
>
>
> On 10/04/2019 16:54, Michel Haber wrote:
>
> Hello Sylvain, and thanks again :)
>
> When adding the forall I can compile the code without a problem.
>
> For the types b1 b2 b3, they are of course not what I want (b must be
> unique in the context of the question).
> But the type for the function with b1, b2 and b3 is what I got when I did
> not give a type signature to the compiler/interpreter (which is
> understandable since it has no reason to assume they would be one and the
> same).
>
> I will try the Functional dependency (though I haven't learned about this
> yet).
>
> But the main question remains:
>
> "add x y = wrap $ unwrap x + unwrap y" can be compiled/interpreted, and
> when I ask about its type, the answer is:
> ":t add"
> "add :: (Num a, Newtype a b1, Newtype a b2, Newtype a b3) => b2 -> b3 ->
> b1"
>
> Then when I add that same type signature, like so:
> "add :: (Num a, Newtype a b1, Newtype a b2, Newtype a b3) => b2 -> b3 -> b1
> add x y = wrap $ unwrap x + unwrap y"
> the compiler refuses it for ambiguity reasons.
>
> So the question is: How come the compiler does not accept its own type
> signature? Why had it not refused to compile even without one, and only
> upon specification of said signature did the compilation break?
>
> Regards,
> Michel :)
>
> On Wed, Apr 10, 2019 at 4:29 PM Sylvain Henry <sylvain at haskus.fr> wrote:
>
>>
>> On 10/04/2019 15:29, Michel Haber wrote:
>>
>> Hello,
>> Thanks for the answer.
>> I tried the code you sent, but now I'm getting a "type variable not in
>> score" error. (I added both extensions)
>> This is the whole code pertaining to this problem (with the extensions
>> mentioned before):
>>
>> class Newtype a b where
>> wrap :: a -> b
>> unwrap :: b -> a
>>
>> newtype MyInt = MyInt Int
>> newtype YourInt = YourInt Int
>>
>> instance Newtype Int MyInt where
>> wrap = MyInt
>> unwrap (MyInt i) = i
>>
>> instance Newtype Int YourInt where
>> wrap = YourInt
>> unwrap (YourInt i) = i
>>
>> add :: (Num a, Newtype a b1, Newtype a b2, Newtype a b3) => b2 -> b3 -> b1
>> add x y = wrap @a @b1 $ unwrap @a x + unwrap @a y
>>
>> You need to add the "forall a b1 b2 b3" to be allowed to use "@a" (with
>> ScopedTypeVariables extension).
>>
>>
>> For further reference, the exercice to which this code should be a
>> solution can be found at:
>>
>> https://github.com/i-am-tom/haskell-exercises/blob/answers/09-MultiParamTypeClasses/src/Exercises.hs
>>
>> > c. Write a function that adds together two values of the same type, providing
>> that the type is a newtype around some type with a 'Num' instance.
>>
>> You only need a single "b" type instead of b1, b2 b3. Also I think you
>> could use a Function Dependency in the "Newtype" definition (because when
>> we know "b" we know "a"). It will make the code of "add' much simpler.
>>
>>
>> Finally, the question remains: Is it "normal" that ghci behave
>> differently depending on whether
>> the type signature is declared or not? (Remember that the signature is
>> given by ghci itself)
>>
>> Finally it is not related to GHCi (we get the same errors/warnings when
>> we compile) but to the AllowAmbiguousTypes extension:
>> https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html?#extension-AllowAmbiguousTypes
>>
>> The type of "add" is ambiguous according to the definition in the manual.
>>
>>
>> My advice would be to use a Functional dependency in your definition of
>> NewType and then you can forget about ambiguous types, type applications,
>> scoped type variables, etc. for now. The reported type of "add" by ghci
>> becomes non-ambiguous and everything is well :) (and I guess that it was
>> the point of the exercise)
>>
>> Regards,
>> Sylvain
>>
>>
>>
>> Thanks again,
>> Michel :)
>>
>> On Wed, Apr 10, 2019 at 1:28 PM Sylvain Henry <sylvain at haskus.fr> wrote:
>>
>>> Hi,
>>>
>>> It looks like an effect of ExtendedDefaultRules:
>>> https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/ghci.html#extension-ExtendedDefaultRules
>>>
>>> It's hard to tell without the code but maybe something like that will do:
>>>
>>> {-# LANGUAGE ScopedTypeVariables #-}
>>> {-# LANGUAGE TypeApplications #-}
>>>
>>> add :: forall a b1 b2 b3. (Num a, Newtype a b1, Newtype a b2, Newtype a
>>> b3) => b2 -> b3 -> b1
>>> add x y = wrap @a @b1 $ unwrap @a x + unwrap @a y
>>>
>>> -Sylvain
>>> On 10/04/2019 12:32, Michel Haber wrote:
>>>
>>> Hello Cafe,
>>>
>>> I was trying to load a module containing this function in ghci:
>>> "add x y = wrap $ unwrap x + unwrap y"
>>> with the following extensions activated:
>>>
>>> ConstraintKinds
>>> DataKinds
>>> DeriveFunctor
>>> DuplicateRecordFields
>>> FlexibleContexts
>>> FlexibleInstances
>>> GADTs
>>> KindSignatures
>>> MultiParamTypeClasses
>>> PolyKinds
>>> TypeFamilies
>>> TypeOperators
>>> AllowAmbiguousTypes
>>>
>>> And it loaded without problem.
>>>
>>> So then I tested its type with ":t add", which gave:
>>> add :: (Num a, Newtype a b1, Newtype a b2, Newtype a b3) => b2 -> b3 ->
>>> b1
>>>
>>> Then I added this signature to the function in the module. This caused
>>> ghci
>>> to refuse to load it and give the following error:
>>>
>>> src/Exercises.hs:55:11: error:
>>> • Could not deduce (Newtype Integer b1)
>>> arising from a use of ‘wrap’
>>> from the context: (Num a, Newtype a b1, Newtype a b2, Newtype a b3)
>>> bound by the type signature for:
>>> add :: forall a b1 b2 b3.
>>> (Num a, Newtype a b1, Newtype a b2, Newtype a
>>> b3) =>
>>> b2 -> b3 -> b1
>>> at src/Exercises.hs:54:1-74
>>> • In the expression: wrap $ unwrap x + unwrap y
>>> In an equation for ‘add’: add x y = wrap $ unwrap x + unwrap y
>>> |
>>> 55 | add x y = wrap $ unwrap x + unwrap y
>>> | ^^^^^^^^^^^^^^^^^^^^^^^^^^
>>>
>>> src/Exercises.hs:55:18: error:
>>> • Could not deduce (Newtype Integer b2)
>>> arising from a use of ‘unwrap’
>>> from the context: (Num a, Newtype a b1, Newtype a b2, Newtype a b3)
>>> bound by the type signature for:
>>> add :: forall a b1 b2 b3.
>>> (Num a, Newtype a b1, Newtype a b2, Newtype a
>>> b3) =>
>>> b2 -> b3 -> b1
>>> at src/Exercises.hs:54:1-74
>>> • In the first argument of ‘(+)’, namely ‘unwrap x’
>>> In the second argument of ‘($)’, namely ‘unwrap x + unwrap y’
>>> In the expression: wrap $ unwrap x + unwrap y
>>> |
>>> 55 | add x y = wrap $ unwrap x + unwrap y
>>> | ^^^^^^^^
>>>
>>> src/Exercises.hs:55:29: error:
>>> • Could not deduce (Newtype Integer b3)
>>> arising from a use of ‘unwrap’
>>> from the context: (Num a, Newtype a b1, Newtype a b2, Newtype a b3)
>>> bound by the type signature for:
>>> add :: forall a b1 b2 b3.
>>> (Num a, Newtype a b1, Newtype a b2, Newtype a
>>> b3) =>
>>> b2 -> b3 -> b1
>>> at src/Exercises.hs:54:1-74
>>> • In the second argument of ‘(+)’, namely ‘unwrap y’
>>> In the second argument of ‘($)’, namely ‘unwrap x + unwrap y’
>>> In the expression: wrap $ unwrap x + unwrap y
>>> |
>>> 55 | add x y = wrap $ unwrap x + unwrap y
>>> | ^^^^^^^^
>>> Failed, no modules loaded.
>>>
>>> This does not make sense to me, since I only used the signature that
>>> ghci itself gave me.
>>>
>>> Is this a bug? if not, could someone please explain this behaviour to me?
>>>
>>> Thanks,
>>> Michel
>>>
>>> _______________________________________________
>>> Haskell-Cafe mailing list
>>> To (un)subscribe, modify options or view archives go to:http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>>> Only members subscribed via the mailman list are allowed to post.
>>>
>>> _______________________________________________
>>> Haskell-Cafe mailing list
>>> To (un)subscribe, modify options or view archives go to:
>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>>> Only members subscribed via the mailman list are allowed to post.
>>
>> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.
--
brandon s allbery kf8nh
allbery.b at gmail.com
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20190410/837fa40f/attachment.html>
More information about the Haskell-Cafe
mailing list