confusing type error
I recently got a confusing error msg, and reduced it to a small case: f1 :: Monad m = m Bool f1 = f2 0 0 'a' f2 :: Monad m = Int - Float - m Bool f2 = undefined From this, it's clear that f2 is being given an extra Char argument it didn't ask for. However, the error msg (ghc 7.8.3) is: Couldn't match type ‘m Bool’ with ‘Bool’ Expected type: Char - m Bool Actual type: Char - Bool Relevant bindings include f1 :: m Bool (bound at Bug.hs:4:1) The function ‘f2’ is applied to three arguments, but its type ‘Int - Float - Char - Bool’ has only three In the expression: f2 0 0 'a' In an equation for ‘f1’: f1 = f2 0 0 'a' The confusing part is that 'f2' was applied to three arguments, but it's type has only three. It includes the Char in expected and actual types, and implies that the type of 'f2' includes the Char. So I took quite a while to realize that the type of 'f2' in fact *didn't* expect a Char (and had an 'm'), so that the but its type is *not* in fact its declared type. I suppose it infers a type for 'f2' based on its use, and that then becomes the actual type, but it seems less confusing if it picked the declared type of 'f2' as its actual type. Perhaps this is working as intended, but it it is confusing! Especially the part about expected three but got three. Ideally I'd like to see too many arguments or at least expected (Char - m Bool) but actually 'm Bool'. Actually I'd expect the other way: expected 'm Bool' but got (Char - m Bool)' but I think ghc has always done it backwards from how I expect. It looks like it's substituting (-) for 'm', so maybe it's one of those things where ((-) a) is also a monad. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: confusing type error
This seems straightforwardly to be a bug, to me. HEAD gives the same behavior you report below. Please post on the bug tracker at https://ghc.haskell.org/trac/ghc/newticket Thanks! Richard On Dec 4, 2014, at 1:50 PM, Evan Laforge qdun...@gmail.com wrote: I recently got a confusing error msg, and reduced it to a small case: f1 :: Monad m = m Bool f1 = f2 0 0 'a' f2 :: Monad m = Int - Float - m Bool f2 = undefined From this, it's clear that f2 is being given an extra Char argument it didn't ask for. However, the error msg (ghc 7.8.3) is: Couldn't match type ‘m Bool’ with ‘Bool’ Expected type: Char - m Bool Actual type: Char - Bool Relevant bindings include f1 :: m Bool (bound at Bug.hs:4:1) The function ‘f2’ is applied to three arguments, but its type ‘Int - Float - Char - Bool’ has only three In the expression: f2 0 0 'a' In an equation for ‘f1’: f1 = f2 0 0 'a' The confusing part is that 'f2' was applied to three arguments, but it's type has only three. It includes the Char in expected and actual types, and implies that the type of 'f2' includes the Char. So I took quite a while to realize that the type of 'f2' in fact *didn't* expect a Char (and had an 'm'), so that the but its type is *not* in fact its declared type. I suppose it infers a type for 'f2' based on its use, and that then becomes the actual type, but it seems less confusing if it picked the declared type of 'f2' as its actual type. Perhaps this is working as intended, but it it is confusing! Especially the part about expected three but got three. Ideally I'd like to see too many arguments or at least expected (Char - m Bool) but actually 'm Bool'. Actually I'd expect the other way: expected 'm Bool' but got (Char - m Bool)' but I think ghc has always done it backwards from how I expect. It looks like it's substituting (-) for 'm', so maybe it's one of those things where ((-) a) is also a monad. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: confusing type error
Int - Float - Char - Bool *is* in fact a valid type for f2, since ((-) Char) is a Monad. However, I agree the error message is confusing, especially the expected n, but got n part. -Brent On Thu, Dec 4, 2014 at 1:50 PM, Evan Laforge qdun...@gmail.com wrote: I recently got a confusing error msg, and reduced it to a small case: f1 :: Monad m = m Bool f1 = f2 0 0 'a' f2 :: Monad m = Int - Float - m Bool f2 = undefined From this, it's clear that f2 is being given an extra Char argument it didn't ask for. However, the error msg (ghc 7.8.3) is: Couldn't match type ‘m Bool’ with ‘Bool’ Expected type: Char - m Bool Actual type: Char - Bool Relevant bindings include f1 :: m Bool (bound at Bug.hs:4:1) The function ‘f2’ is applied to three arguments, but its type ‘Int - Float - Char - Bool’ has only three In the expression: f2 0 0 'a' In an equation for ‘f1’: f1 = f2 0 0 'a' The confusing part is that 'f2' was applied to three arguments, but it's type has only three. It includes the Char in expected and actual types, and implies that the type of 'f2' includes the Char. So I took quite a while to realize that the type of 'f2' in fact *didn't* expect a Char (and had an 'm'), so that the but its type is *not* in fact its declared type. I suppose it infers a type for 'f2' based on its use, and that then becomes the actual type, but it seems less confusing if it picked the declared type of 'f2' as its actual type. Perhaps this is working as intended, but it it is confusing! Especially the part about expected three but got three. Ideally I'd like to see too many arguments or at least expected (Char - m Bool) but actually 'm Bool'. Actually I'd expect the other way: expected 'm Bool' but got (Char - m Bool)' but I think ghc has always done it backwards from how I expect. It looks like it's substituting (-) for 'm', so maybe it's one of those things where ((-) a) is also a monad. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: confusing type error
I don't see a bug here. f2 is perfectly OK, so, let's examine f1 more closely. It tries to get `m Bool` by applying f1 to three arguments: 0, 0, and 'a'. Now, since `f2` has the type `Int - Float - n Bool`, where `n` is of kind `* - *` (and an instance of `Monad` class, but it's not yet the time to look for instances), we have `f2 0 :: Float - n Bool` and `f2 0 0 :: n Bool`. Since that is applied to 'a', Haskell deduces that the last type should be something like `Char - Something` — or, equivalently, `(-) Char Something`. Therefore, it can see that `n` is in fact `(-) Char` and `Something` is `Bool`. Therefore, `f2 0 0 'a' :: Bool`. But it is expecting `m Bool`, not `Bool` — which is exactly what an error message says. Отправлено с iPad 4 дек. 2014 г., в 21:50, Evan Laforge qdun...@gmail.com написал(а): I recently got a confusing error msg, and reduced it to a small case: f1 :: Monad m = m Bool f1 = f2 0 0 'a' f2 :: Monad m = Int - Float - m Bool f2 = undefined From this, it's clear that f2 is being given an extra Char argument it didn't ask for. However, the error msg (ghc 7.8.3) is: Couldn't match type ‘m Bool’ with ‘Bool’ Expected type: Char - m Bool Actual type: Char - Bool Relevant bindings include f1 :: m Bool (bound at Bug.hs:4:1) The function ‘f2’ is applied to three arguments, but its type ‘Int - Float - Char - Bool’ has only three In the expression: f2 0 0 'a' In an equation for ‘f1’: f1 = f2 0 0 'a' The confusing part is that 'f2' was applied to three arguments, but it's type has only three. It includes the Char in expected and actual types, and implies that the type of 'f2' includes the Char. So I took quite a while to realize that the type of 'f2' in fact *didn't* expect a Char (and had an 'm'), so that the but its type is *not* in fact its declared type. I suppose it infers a type for 'f2' based on its use, and that then becomes the actual type, but it seems less confusing if it picked the declared type of 'f2' as its actual type. Perhaps this is working as intended, but it it is confusing! Especially the part about expected three but got three. Ideally I'd like to see too many arguments or at least expected (Char - m Bool) but actually 'm Bool'. Actually I'd expect the other way: expected 'm Bool' but got (Char - m Bool)' but I think ghc has always done it backwards from how I expect. It looks like it's substituting (-) for 'm', so maybe it's one of those things where ((-) a) is also a monad. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: confusing type error
It seems to be an instance of https://ghc.haskell.org/trac/ghc/ticket/7869 But it is fixed (both in HEAD and 7.8). Probably the fix is partial? On Thu, 2014-12-04 at 14:53 -0500, Richard Eisenberg wrote: This seems straightforwardly to be a bug, to me. HEAD gives the same behavior you report below. Please post on the bug tracker at https://ghc.haskell.org/trac/ghc/newticket Thanks! Richard On Dec 4, 2014, at 1:50 PM, Evan Laforge qdun...@gmail.com wrote: I recently got a confusing error msg, and reduced it to a small case: f1 :: Monad m = m Bool f1 = f2 0 0 'a' f2 :: Monad m = Int - Float - m Bool f2 = undefined From this, it's clear that f2 is being given an extra Char argument it didn't ask for. However, the error msg (ghc 7.8.3) is: Couldn't match type ‘m Bool’ with ‘Bool’ Expected type: Char - m Bool Actual type: Char - Bool Relevant bindings include f1 :: m Bool (bound at Bug.hs:4:1) The function ‘f2’ is applied to three arguments, but its type ‘Int - Float - Char - Bool’ has only three In the expression: f2 0 0 'a' In an equation for ‘f1’: f1 = f2 0 0 'a' The confusing part is that 'f2' was applied to three arguments, but it's type has only three. It includes the Char in expected and actual types, and implies that the type of 'f2' includes the Char. So I took quite a while to realize that the type of 'f2' in fact *didn't* expect a Char (and had an 'm'), so that the but its type is *not* in fact its declared type. I suppose it infers a type for 'f2' based on its use, and that then becomes the actual type, but it seems less confusing if it picked the declared type of 'f2' as its actual type. Perhaps this is working as intended, but it it is confusing! Especially the part about expected three but got three. Ideally I'd like to see too many arguments or at least expected (Char - m Bool) but actually 'm Bool'. Actually I'd expect the other way: expected 'm Bool' but got (Char - m Bool)' but I think ghc has always done it backwards from how I expect. It looks like it's substituting (-) for 'm', so maybe it's one of those things where ((-) a) is also a monad. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: confusing type error
On Thu, Dec 4, 2014 at 12:59 PM, migmit mig...@gmail.com wrote: It tries to get `m Bool` by applying f1 to three arguments: 0, 0, and 'a'. Now, since `f2` has the type `Int - Float - n Bool`, where `n` is of kind `* - *` (and an instance of `Monad` class, but it's not yet the time to look for instances), we have `f2 0 :: Float - n Bool` and `f2 0 0 :: n Bool`. Since that is applied to 'a', Haskell deduces that the last type should be something like `Char - Something` — or, equivalently, `(-) Char Something`. Therefore, it can see that `n` is in fact `(-) Char` and `Something` is `Bool`. Therefore, `f2 0 0 'a' :: Bool`. But it is expecting `m Bool`, not `Bool` — which is exactly what an error message says. Right, that's what I suspected was happening. The confusion arrises because it guesses that 'm' should be (-), and that deduction then leads to a dead-end. But when it reports the problem, it uses its guessed 'm', rather that backing up to the declared value. But surely always backing up to the declared unspecialized value is no good either, because then you get vague errors. All the compiler knows is that when it simplifies as far as it can, it winds up with a /= b, it doesn't know that I would have been surprised by its path a few steps back. But arity errors are common, and intentionally instantiating a prefix type constructor like 'm a' as (-) is probably much less common. So perhaps there could be a heuristic that treats (-) specially and includes an extra clause in the error if it unified a type variable to (-)? I suspect the expected n but got n error is also due to the same thing, it counts arrows on one side but inferred arrows on the other? Or something? In any case, it seems like the two sides are counting inconsistently. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Proving properties of type-level natural numbers obtained from user input
Hi, Richard
Can you give some ideas or where to read how to properly use signletons
and unary naturals in order to be able to express such constraints?
Thanks
--
Alexander
On 30 November 2014 at 23:26, Richard Eisenberg e...@cis.upenn.edu wrote:
Hi Alexander,
Nice idea to test against the set of known values. That's more type-safe than
anything I've thought of. I agree that it's a bit of a painful construction,
but I don't think we can do better with type-lits, as there is limited
reasoning ability that GHC can manage. If you want to switch to unary
naturals (`data Nat = Zero | Succ Nat`), then this can be built somewhat
nicely with singletons and without unsafeCoerce. But, of course, unary
naturals are very slow.
By the way, the bug in the Proof2 version is a bug in GHC 7.8.3 (only in .3
-- not in .2 or in the soon-to-be .4) that allows you to write unsaturated
type families that don't work. Saying `LessThan255` without a parameter
should be a syntax error, but that check was accidentally turned off for
7.8.3, leading to a bogus type error.
Thanks for sharing this work!
Richard
On Nov 28, 2014, at 5:27 PM, Alexander V Vershilov
alexander.vershi...@gmail.com wrote:
Hi, Bas, Richard.
I've played a bit with example, obvously first approach contained bugs,
but seems that I have fixed it and here I have 2 approaches, one uses
unsafeCoerce (as Richard suggested) another is safe but with bad complexity:
Full file is quite big, so I'm not inlining it in mail, but here is a link:
https://github.com/qnikst/haskell-fun/blob/master/typelevel-literals/Proof.lhs
I wonder how far it's possible to go with singletons approach that I have
not tried yet.
--
Alexander
On 26 November 2014 at 10:15, Bas van Dijk v.dijk@gmail.com wrote:
Hi Alexander,
Thanks for your answer! This provides a lot of ideas how to proceed.
I'm unsure about the following though:
lessThen :: KnownNat m = SomeNat - Proxy m - Maybe (Proof (n = m)
(Proxy n))
lessThen (SomeNat p) k
| natVal p = natVal k = Just (Proof $ Tagged (Proxy :: Proxy n))
| otherwise = Nothing
Doesn't this mean lessThen returns a Proxy n for all (n :: Nat) and
not just the Nat inside the SomeNat?
I also see that p is only used for comparing it to k. It's not used to
produce the return value.
Cheers,
Bas
On 25 November 2014 at 19:55, Alexander V Vershilov
alexander.vershi...@gmail.com wrote:
Hi, Richard, Bas.
Maybe I didn't spell it properly but my point was to create a data
type that carry a proof
without exposing it's constructor and having clever constructor only,
then the only place
where you need to check will be that constructor.
Also it's possible to write in slightly clearer, but again it's
possible to make a mistake here
and it will be a false proof.
lessThen :: KnownNat m = SomeNat - Proxy m - Maybe (Proof (n = m)
(Proxy n))
lessThen (SomeNat p) k
| natVal p = natVal k = Just (Proof $ Tagged (Proxy :: Proxy n))
| otherwise = Nothing
Of cause solution using singletons could solve this problem much better.
--
Alexander
On 25 November 2014 at 21:34, Richard Eisenberg e...@cis.upenn.edu wrote:
Hi Bas,
I believe to do this right, you would need singleton types. Then, when
you discover that the number is bounded by 255, you would also discover
that the type is bounded by 255, and you'd be home free.
Unfortunately, I there isn't currently a way to do comparison on
GHC.TypeLits Nats with singletons. (There is a module
Data.Singletons.TypeLits in the `singletons` package, but there's a
comment telling me TODO in the part where comparison should be
implemented.) If it were implemented, it would have to use unsafeCoerce,
as there's no built-in mechanism connecting runtime numbers with TypeLits.
If I were you, I would just write `g` using unsafeCoerce in the right
spot, instead of bothering with all the singletons, which would have to
use unsafety anyway.
The solution Alexander provides below doesn't quite build a proof, I
think. Tellingly, if we omit the `natVal p = 255` check, everything else
still compiles. Thus, the `Proof` type he uses can be built even if the
fact proven is false. That said, I don't know if my solution is any
better, crucially relying on unsafeCoerce.
Richard
On Nov 25, 2014, at 4:52 AM, Alexander V Vershilov
alexander.vershi...@gmail.com wrote:
Hi,
Following approach can work, the idea is to define a type that will
carry a proof (constraint) that we want to check. Here I have reused
Data.Tagged, but it's possible to introduce your own with concrete
constraints.
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE UndecidableInstances #-}
import GHC.TypeLits
import GHC.Exts
import Data.Proxy
import Data.Tagged
import System.Environment
New constraint carrying data type
newtype Proof a
