Opened 12 months ago

Last modified 10 months ago

#15674 new feature request

GADT's displayed type is misleading

Reported by: AntC Owned by:
Priority: normal Milestone: 8.6.1
Component: Compiler Version: 8.6.1-beta1
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Poor/confusing error message Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

GHCi's :t alleges these three data constructors have the same type :: Int -> T Int (modulo name of the type constructor):

data DG a where MkDG  ::            Int -> DG Int 
                MkDG2 :: (a ~ Int) => a -> DG a

data family DF a
data instance DF Int where MkDF ::  Int -> DF Int

I tried switching on verbosity flags, but to no avail: -fprint-explicit-foralls, -fprint-equality-relations, and a few others.

The DG constructors are GADTs, the DF constructor is not. So it's not hard to see different type-level behaviour:

f (MkDF  x) = x                   -- accepted without a signature
-- f :: DF Int -> Int             -- inferred signature, or you can spec it
-- f :: DF a   -> a               -- rejected: signature is too general/
                                  -- a is a rigid type variable

g (MkDG  x) = x                   -- } without a signature, rejected
g (MkDG2 x) = x                   -- } "untouchable" type (Note)

-- g :: DG Int -> Int             -- } g accepted with either sig 
-- g :: DG a   -> a               -- } ?but MkDG doesn't return DG a, allegedly

Note: at least the error message re MkDG2 does show its type as :: (forall a). (a ~ Int) => DG a -> a. But doggedly MkDG :: Int -> DG Int.

"Untouchable" error messages are a fertile source of questions on StackOverflow. The message does say Possible fix: add a type signature for 'g', but gives no clue what the signature might be.

If you've imported these data constructors from a library, such that you can't (easily) see they're GADTs, couldn't :t give you better help to show what's going on? Or should one of the verbosity flags already do this?

Change History (8)

comment:1 Changed 12 months ago by simonpj

:type <expr> tells you the type of the expression <expr>, where <expr> can be any old expression, not just a single identifier.

On the other hand :info <name> gives you information about the declaration of the entity <name>. And indeed :info MkDF, :info MkDG and :info MkDG2 give you the info that I think you want. This works if the constructors are imported from a library that you can't (easily) see.

Does that help?

Perhaps :t should behave precisely like :i if it is given a single identifier as its argument. That would be non-uniform and ad-hoc, but perhaps useful in practice.

Last edited 12 months ago by simonpj (previous) (diff)

comment:2 in reply to:  1 ; Changed 12 months ago by AntC

Replying to simonpj:

Thank you Simon.

:type <expr> tells you the type of the expression <expr>, where <expr> can be any old expression, not just a single identifier.

Yes. So you're saying those three data constructors are at the same type, considered as expressions(?) What is it about their typedness that explains the observable difference in behaviour wrt the functions? (It's to do with pattern matching/deconstructing, rather than applying them as functions/constructing.)

On the other hand :info <name> gives you information about the declaration of the entity <name>.

Yes, :info more or less shows the code that declares <name>.

And indeed :info MkDF, :info MkDG and :info MkDG2 give you the info that I think you want.

Hmm. :info still shows MkDF :: Int -> DF Int, MkDG :: Int -> DG Int. It does show MkDG2 :: (a ~ Int) => a -> DG a or even MkDG2 :: forall a. (a ~ Int) => a -> DG a.

So prima facie MkDF, MkDG's types are the same; MkDG2's is different. But actually MkDG is the same as MkDG2. (And setting -fprint-explicit-foralls doesn't explicitly show the forall in MkDG, although it does in MkDG2. But MkDG2's decl doesn't have an explicit forall, neither do I need -XExplicitForAll to compile it -- that's not implied by -XGADTs, surprisingly.)

This works if the constructors are imported from a library that you can't (easily) see.

Ok.

Does that help?

Perhaps :t should behave precisely like :i if it is given a single identifier as its argument. That would be non-uniform and ad-hoc, but perhaps useful in practice.

Usually if I'm having trouble from error messages to do with "untouchable" or "rigid", it's :t I go to. I just have to kick myself to go to :i. But even the type signature showing in :i is misleading. Perhaps: if <name> is a data constructor, and not a H98 constructor, and -fprint-explicit-foralls is set, show the foralls explicitly?

comment:3 in reply to:  2 ; Changed 12 months ago by goldfire

Replying to AntC:

(It's to do with pattern matching/deconstructing, rather than applying them as functions/constructing.)

Precisely.

So prima facie MkDF, MkDG's types are the same; MkDG2's is different.

This is true.

But actually MkDG is the same as MkDG2.

In most contexts, yes. But you can say MkDG2 @Int while you can't do that with MkDG. Their types are subtly different.

(And setting -fprint-explicit-foralls doesn't explicitly show the forall in MkDG, although it does in MkDG2.

There is no forall in MkDG, which doesn't quantify over any variables.

But MkDG2's decl doesn't have an explicit forall, neither do I need -XExplicitForAll to compile it -- that's not implied by -XGADTs, surprisingly.)

Your code does not contain an explicit forall in MkDG2. It contains an implicit one, implied by the presence of the type variable a.

Does that help?

Perhaps :t should behave precisely like :i if it is given a single identifier as its argument. That would be non-uniform and ad-hoc, but perhaps useful in practice.

But that would be non-uniform and ad-hoc. :)

:type <expr> gives you the type that is assigned to it if you had let it = <expr>. It's a uniform rule that always works.

Usually if I'm having trouble from error messages to do with "untouchable" or "rigid", it's :t I go to. I just have to kick myself to go to :i. But even the type signature showing in :i is misleading. Perhaps: if <name> is a data constructor, and not a H98 constructor, and -fprint-explicit-foralls is set, show the foralls explicitly?

I'm not sure what foralls you're looking for. There isn't one in MkDG.

comment:4 Changed 12 months ago by monoidal

One way to see the difference is to define

pattern PDG a = MkDG a
pattern PDG2 a = MkDG2 a
pattern PDF a = MkDF a

then :i PDG PDG2 PDF will show

pattern PDG :: () => (a ~ Int) => Int -> DG a
  	-- Defined at GA.hs:8:1
pattern PDG2 :: () => (a ~ Int) => a -> DG a
  	-- Defined at GA.hs:9:1
pattern PDF :: Int -> DF Int 	-- Defined at GA.hs:10:1

Should we show this and how? I don't know.

comment:5 in reply to:  3 ; Changed 12 months ago by AntC

Replying to goldfire:

... you can say MkDG2 @Int while you can't do that with MkDG. Their types are subtly different.

Aagh. My brain just blew a fuse.

(And setting -fprint-explicit-foralls doesn't explicitly show the forall in MkDG, although it does in MkDG2.

There is no forall in MkDG, which doesn't quantify over any variables.

Then I totally ignore the a in the data DG a where ...? (I don't mean its specific variable name, I mean the fact that MkDG's return type is more specific that the data's head, which is what makes it a GADT.)

But MkDG2's decl doesn't have an explicit forall, neither do I need -XExplicitForAll to compile it -- that's not implied by -XGADTs, surprisingly.)

Your code does not contain an explicit forall in MkDG2. It contains an implicit one, implied by the presence of the type variable a.

For MkDG2, with -fprint-explicit-foralls

:i shows MkDG2 :: forall a. (a ~ Int) => a -> DG a

:t shows MkDG2 :: Int -> DG Int

With -fno-print-explicit-foralls

:i shows MkDG2 :: (a ~ Int) => a -> DG a

:t shows MkDG2 :: Int -> DG Int

Is that intended behaviour? It doesn't seem either internally consistent, nor consistent with your explanation: why is the forall appearing at all? Why is it appearing for :i but not :t?

For :t, why is the (a ~ Int) not showing, even with verbosity to the max? MkDG2's decl does have that explicitly, and it does make a (subtle) difference to the type.

I'm not sure what foralls you're looking for. There isn't one in MkDG.

What I'm looking for with these mind-blowingly similar-but- "subtly different" nuances is strong help from the compiler to navigate error messages when I get my types wrong. (Or rather, when I get wrong the types I'm importing from some library whose internals I don't really want to tangle with.)

comment:6 in reply to:  4 Changed 12 months ago by AntC

Replying to monoidal:

Thank you for the tip with defining patterns. It's the only way to reveal the differences here:

data family   DG3  a
data instance DG3  a   where MkDG3 :: Int -> DG3 [Int]

data family   DG4  a
data instance DG4 [a]  where MkDG4 :: Int -> DG4 [Int]

> :i  PDG3  PDG4

pattern PDG3 :: () => (a ~ [Int]) => Int -> DG3 a

pattern PDG4 :: () => (a ~ Int) => Int -> DG4 [a]

Should we show this and how? I don't know.

Now we have variable a showing. But according to Richard's message, it shouldn't be because it's not forall'd, neither explicitly nor implicitly (sigh). And indeed :i for the data constructors doesn't show (a ~ ...) even with full verbosity.

My understanding of pattern synonyms is that they're built on top of data constructors. Then it seems back-to-front to use pattern synonyms to diagnose constructors. This ticket arose from a quest to understand data and data instances from the ground up. I can't find any firm ground to start from, only quicksand.

comment:7 in reply to:  5 Changed 12 months ago by goldfire

Replying to AntC:

There is no forall in MkDG, which doesn't quantify over any variables.

Then I totally ignore the a in the data DG a where ...?

In GADT syntax, the bit between the data and the where is the declaration for the type only -- not any constructors. The a there serves to say that DG takes one argument. It does not affect or cause any variable quantification in constructors.

For MkDG2, with -fprint-explicit-foralls

:i shows MkDG2 :: forall a. (a ~ Int) => a -> DG a

:t shows MkDG2 :: Int -> DG Int

With -fno-print-explicit-foralls

:i shows MkDG2 :: (a ~ Int) => a -> DG a

:t shows MkDG2 :: Int -> DG Int

Is that intended behaviour? It doesn't seem either internally consistent, nor consistent with your explanation: why is the forall appearing at all? Why is it appearing for :i but not :t?

Yes, this is all expected behavior. Haskell allows you omit foralls if you have a type variable in a type. But when you write -fprint-explicit-foralls, it will print one even if you left it out. So: the forall appears because you asked for it.

I'll quote myself:

:type <expr> gives you the type that is assigned to it if you had let it = <expr>. It's a uniform rule that always works.

When we say let it = MkDG2, GHC instantiates the type of MkDG2 at its occurrence and then generalizes (because let-bound variables are generalized). Thus, it might not have exactly the same type as MkDG2, which is what's happening here.

Here's a simpler example:

silly :: (Ord a, Eq a) => a -> Bool
silly = ...

Asking for :t silly gives you Ord a => a -> Bool. This is because we instantiate and regeneralize the type of silly. In this process, GHC realizes that Eq a is redundant and drops it. The same is happening with MkDG2.

What I'm looking for with these mind-blowingly similar-but- "subtly different" nuances is strong help from the compiler to navigate error messages when I get my types wrong.

Short of a use of a type application (which doesn't seem to be what you're doing), MkDG and MkDG2 behave identically.

comment:8 Changed 10 months ago by Phyx-

Architecture: x86_64 (amd64)Unknown/Multiple
Operating System: WindowsUnknown/Multiple

Not a Windows specific issue, reclassifying.

Note: See TracTickets for help on using tickets.