
I’ve been working through Typing Haskell in Haskell in detail ( https://gist.github.com/chrisdone/0075a16b32bfd4f62b7b), and I noticed that if I change e.g. SourcePrelude.hs from the Hackage package ( http://hackage.haskell.org/package/thih) to have a declaration like this: [("printZ", Just (Forall [] ([] :=> (tString))), [([], ap [econst showMfun, econst (("Z" :>: toScheme (TCon (Tycon "Nat" Star))))])])], In other words printChar = show (Z :: Nat) Where Z is neither defined nor an instance of Show, it type checks just fine. If I replace it with e.g. toScheme (TVar(Tyvar "k" Star)) i.e. “some thing of type k“, then it complains that the instance is ambiguous, which is true. So it seems that THIH will accept any type as an instance of any class without complaint as long as all the type variables have been filled in with the correct kind. This came as a surprise to me, as I’m using it in a project. There is apparently code in the type checker that pays attention to the class environment, and you provide instances to it, but it doesn’t seem to care what instances are provided or not. I believe I’ll have to do some extra work to check that the instances actually exist and are full resolved. I can’t tell whether this is a bug or intended behavior. I tried emailing the author of THIH but his email bounced back. Frankly the actual interesting bit of the type checker — the bit where we resolve class instances — is actually the hardest bit for me to read and the bit I’d like more exposition on. I’ve written a tokenizer, parser, renamer and thanks to THIH an inferer, and a stepper in a small dialect of Haskell I’m calling Duet. There’s an example here: http://chrisdone.com/toys/duet-gamma/ You can see the problem illustrated if you type e.g. the following in the top-left: data Nat = Z | S Natmain = show Z The type inferred is: main = ((show :: (Show Nat) => Nat -> String) (Z :: Nat) :: (Show Nat) => String) Which is at least enough information for me to do a lookup and insert an instance dictionary. But I sort of would have expected the type checker to say “no instance”. It does explicitly say that you have to do your own dependency analysis and renamer, but the instance part isn’t clear to me. Oh, and you also have to write your own kind inference for data type declarations. Who knew implementing a Haskell was so involved? So beware future travelers… THIH is awesome, but these are the things I’ve found missing. Ciao!

Doesn't this more or less mirror the problem with instance visibility that
leads to the orphan instance problem?
On Wed, May 3, 2017 at 2:46 PM, Christopher Done
I’ve been working through Typing Haskell in Haskell in detail ( https://gist.github.com/chrisdone/0075a16b32bfd4f62b7b), and I noticed that if I change e.g. SourcePrelude.hs from the Hackage package ( http://hackage.haskell.org/package/thih) to have a declaration like this:
[("printZ", Just (Forall [] ([] :=> (tString))), [([], ap [econst showMfun, econst (("Z" :>: toScheme (TCon (Tycon "Nat" Star))))])])],
In other words
printChar = show (Z :: Nat)
Where Z is neither defined nor an instance of Show, it type checks just fine. If I replace it with e.g. toScheme (TVar(Tyvar "k" Star)) i.e. “some thing of type k“, then it complains that the instance is ambiguous, which is true.
So it seems that THIH will accept any type as an instance of any class without complaint as long as all the type variables have been filled in with the correct kind. This came as a surprise to me, as I’m using it in a project. There is apparently code in the type checker that pays attention to the class environment, and you provide instances to it, but it doesn’t seem to care what instances are provided or not.
I believe I’ll have to do some extra work to check that the instances actually exist and are full resolved. I can’t tell whether this is a bug or intended behavior. I tried emailing the author of THIH but his email bounced back. Frankly the actual interesting bit of the type checker — the bit where we resolve class instances — is actually the hardest bit for me to read and the bit I’d like more exposition on.
I’ve written a tokenizer, parser, renamer and thanks to THIH an inferer, and a stepper in a small dialect of Haskell I’m calling Duet. There’s an example here: http://chrisdone.com/toys/duet-gamma/
You can see the problem illustrated if you type e.g. the following in the top-left:
data Nat = Z | S Natmain = show Z
The type inferred is:
main = ((show :: (Show Nat) => Nat -> String) (Z :: Nat) :: (Show Nat) => String)
Which is at least enough information for me to do a lookup and insert an instance dictionary. But I sort of would have expected the type checker to say “no instance”. It does explicitly say that you have to do your own dependency analysis and renamer, but the instance part isn’t clear to me. Oh, and you also have to write your own kind inference for data type declarations. Who knew implementing a Haskell was so involved?
So beware future travelers… THIH is awesome, but these are the things I’ve found missing.
Ciao!
_______________________________________________ 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 sine nomine associates allbery.b@gmail.com ballbery@sinenomine.net unix, openafs, kerberos, infrastructure, xmonad http://sinenomine.net

Are you speculating that THIH probably intentionally leaves how to resolve
the particular instance for e.g. `Show Bool` as an exercise for the reader,
instead only implementing that Bool satisfies the shape expected for the
class head?
On 3 May 2017 at 19:59, Brandon Allbery
Doesn't this more or less mirror the problem with instance visibility that leads to the orphan instance problem?
On Wed, May 3, 2017 at 2:46 PM, Christopher Done
wrote: I’ve been working through Typing Haskell in Haskell in detail ( https://gist.github.com/chrisdone/0075a16b32bfd4f62b7b), and I noticed that if I change e.g. SourcePrelude.hs from the Hackage package ( http://hackage.haskell.org/package/thih) to have a declaration like this:
[("printZ", Just (Forall [] ([] :=> (tString))), [([], ap [econst showMfun, econst (("Z" :>: toScheme (TCon (Tycon "Nat" Star))))])])],
In other words
printChar = show (Z :: Nat)
Where Z is neither defined nor an instance of Show, it type checks just fine. If I replace it with e.g. toScheme (TVar(Tyvar "k" Star)) i.e. “some thing of type k“, then it complains that the instance is ambiguous, which is true.
So it seems that THIH will accept any type as an instance of any class without complaint as long as all the type variables have been filled in with the correct kind. This came as a surprise to me, as I’m using it in a project. There is apparently code in the type checker that pays attention to the class environment, and you provide instances to it, but it doesn’t seem to care what instances are provided or not.
I believe I’ll have to do some extra work to check that the instances actually exist and are full resolved. I can’t tell whether this is a bug or intended behavior. I tried emailing the author of THIH but his email bounced back. Frankly the actual interesting bit of the type checker — the bit where we resolve class instances — is actually the hardest bit for me to read and the bit I’d like more exposition on.
I’ve written a tokenizer, parser, renamer and thanks to THIH an inferer, and a stepper in a small dialect of Haskell I’m calling Duet. There’s an example here: http://chrisdone.com/toys/duet-gamma/
You can see the problem illustrated if you type e.g. the following in the top-left:
data Nat = Z | S Natmain = show Z
The type inferred is:
main = ((show :: (Show Nat) => Nat -> String) (Z :: Nat) :: (Show Nat) => String)
Which is at least enough information for me to do a lookup and insert an instance dictionary. But I sort of would have expected the type checker to say “no instance”. It does explicitly say that you have to do your own dependency analysis and renamer, but the instance part isn’t clear to me. Oh, and you also have to write your own kind inference for data type declarations. Who knew implementing a Haskell was so involved?
So beware future travelers… THIH is awesome, but these are the things I’ve found missing.
Ciao!
_______________________________________________ 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 sine nomine associates allbery.b@gmail.com ballbery@sinenomine.net unix, openafs, kerberos, infrastructure, xmonad http://sinenomine.net

More that one could argue for two different ways to resolve it: in the
typechecker as you describe, or at link time (that is, we codegen
references to a dictionary and let the linker determine whether said
dictionary exists). Each has drawbacks and advantages.
On Wed, May 3, 2017 at 3:18 PM, Christopher Done
Are you speculating that THIH probably intentionally leaves how to resolve the particular instance for e.g. `Show Bool` as an exercise for the reader, instead only implementing that Bool satisfies the shape expected for the class head?
On 3 May 2017 at 19:59, Brandon Allbery
wrote: Doesn't this more or less mirror the problem with instance visibility that leads to the orphan instance problem?
On Wed, May 3, 2017 at 2:46 PM, Christopher Done
wrote: I’ve been working through Typing Haskell in Haskell in detail ( https://gist.github.com/chrisdone/0075a16b32bfd4f62b7b), and I noticed that if I change e.g. SourcePrelude.hs from the Hackage package ( http://hackage.haskell.org/package/thih) to have a declaration like this:
[("printZ", Just (Forall [] ([] :=> (tString))), [([], ap [econst showMfun, econst (("Z" :>: toScheme (TCon (Tycon "Nat" Star))))])])],
In other words
printChar = show (Z :: Nat)
Where Z is neither defined nor an instance of Show, it type checks just fine. If I replace it with e.g. toScheme (TVar(Tyvar "k" Star)) i.e. “some thing of type k“, then it complains that the instance is ambiguous, which is true.
So it seems that THIH will accept any type as an instance of any class without complaint as long as all the type variables have been filled in with the correct kind. This came as a surprise to me, as I’m using it in a project. There is apparently code in the type checker that pays attention to the class environment, and you provide instances to it, but it doesn’t seem to care what instances are provided or not.
I believe I’ll have to do some extra work to check that the instances actually exist and are full resolved. I can’t tell whether this is a bug or intended behavior. I tried emailing the author of THIH but his email bounced back. Frankly the actual interesting bit of the type checker — the bit where we resolve class instances — is actually the hardest bit for me to read and the bit I’d like more exposition on.
I’ve written a tokenizer, parser, renamer and thanks to THIH an inferer, and a stepper in a small dialect of Haskell I’m calling Duet. There’s an example here: http://chrisdone.com/toys/duet-gamma/
You can see the problem illustrated if you type e.g. the following in the top-left:
data Nat = Z | S Natmain = show Z
The type inferred is:
main = ((show :: (Show Nat) => Nat -> String) (Z :: Nat) :: (Show Nat) => String)
Which is at least enough information for me to do a lookup and insert an instance dictionary. But I sort of would have expected the type checker to say “no instance”. It does explicitly say that you have to do your own dependency analysis and renamer, but the instance part isn’t clear to me. Oh, and you also have to write your own kind inference for data type declarations. Who knew implementing a Haskell was so involved?
So beware future travelers… THIH is awesome, but these are the things I’ve found missing.
Ciao!
_______________________________________________ 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 sine nomine associates allbery.b@gmail.com ballbery@sinenomine.net unix, openafs, kerberos, infrastructure, xmonad http://sinenomine.net
-- brandon s allbery kf8nh sine nomine associates allbery.b@gmail.com ballbery@sinenomine.net unix, openafs, kerberos, infrastructure, xmonad http://sinenomine.net

Good points!
On 3 May 2017 at 20:21, Brandon Allbery
More that one could argue for two different ways to resolve it: in the typechecker as you describe, or at link time (that is, we codegen references to a dictionary and let the linker determine whether said dictionary exists). Each has drawbacks and advantages.
On Wed, May 3, 2017 at 3:18 PM, Christopher Done
wrote: Are you speculating that THIH probably intentionally leaves how to resolve the particular instance for e.g. `Show Bool` as an exercise for the reader, instead only implementing that Bool satisfies the shape expected for the class head?
On 3 May 2017 at 19:59, Brandon Allbery
wrote: Doesn't this more or less mirror the problem with instance visibility that leads to the orphan instance problem?
On Wed, May 3, 2017 at 2:46 PM, Christopher Done
wrote: I’ve been working through Typing Haskell in Haskell in detail ( https://gist.github.com/chrisdone/0075a16b32bfd4f62b7b), and I noticed that if I change e.g. SourcePrelude.hs from the Hackage package ( http://hackage.haskell.org/package/thih) to have a declaration like this:
[("printZ", Just (Forall [] ([] :=> (tString))), [([], ap [econst showMfun, econst (("Z" :>: toScheme (TCon (Tycon "Nat" Star))))])])],
In other words
printChar = show (Z :: Nat)
Where Z is neither defined nor an instance of Show, it type checks just fine. If I replace it with e.g. toScheme (TVar(Tyvar "k" Star)) i.e. “some thing of type k“, then it complains that the instance is ambiguous, which is true.
So it seems that THIH will accept any type as an instance of any class without complaint as long as all the type variables have been filled in with the correct kind. This came as a surprise to me, as I’m using it in a project. There is apparently code in the type checker that pays attention to the class environment, and you provide instances to it, but it doesn’t seem to care what instances are provided or not.
I believe I’ll have to do some extra work to check that the instances actually exist and are full resolved. I can’t tell whether this is a bug or intended behavior. I tried emailing the author of THIH but his email bounced back. Frankly the actual interesting bit of the type checker — the bit where we resolve class instances — is actually the hardest bit for me to read and the bit I’d like more exposition on.
I’ve written a tokenizer, parser, renamer and thanks to THIH an inferer, and a stepper in a small dialect of Haskell I’m calling Duet. There’s an example here: http://chrisdone.com/toys/duet-gamma/
You can see the problem illustrated if you type e.g. the following in the top-left:
data Nat = Z | S Natmain = show Z
The type inferred is:
main = ((show :: (Show Nat) => Nat -> String) (Z :: Nat) :: (Show Nat) => String)
Which is at least enough information for me to do a lookup and insert an instance dictionary. But I sort of would have expected the type checker to say “no instance”. It does explicitly say that you have to do your own dependency analysis and renamer, but the instance part isn’t clear to me. Oh, and you also have to write your own kind inference for data type declarations. Who knew implementing a Haskell was so involved?
So beware future travelers… THIH is awesome, but these are the things I’ve found missing.
Ciao!
_______________________________________________ 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 sine nomine associates allbery.b@gmail.com ballbery@sinenomine.net unix, openafs, kerberos, infrastructure, xmonad http://sinenomine.net
-- brandon s allbery kf8nh sine nomine associates allbery.b@gmail.com ballbery@sinenomine.net unix, openafs, kerberos, infrastructure, xmonad http://sinenomine.net
participants (2)
-
Brandon Allbery
-
Christopher Done