[GHC] #12853: Unpromoted tuples in TH in correctly accepted by tthe type checker
#12853: Unpromoted tuples in TH in correctly accepted by tthe type checker -------------------------------------+------------------------------------- Reporter: erikd | Owner: Type: bug | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler | Version: 8.1 (Type checker) | Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: Other Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- This issue was discovered when writing tests for #11629. Test case: {{{#!hs {-# LANGUAGE DataKinds #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE FlexibleInstances #-} module T11629 where import Control.Monad import Language.Haskell.TH class C (a :: Bool) class D (a :: (Bool, Bool)) class E (a :: [Bool]) instance C True instance C 'False instance D '(True, False) instance D '(False, True) instance E '[True, False] instance E '[False, True] do let getType (InstanceD _ _ ty _) = ty getType _ = error "getType: only defined for InstanceD" failMsg a ty1 ty2 = fail $ "example " ++ a ++ ": ty1 /= ty2, where\n ty1 = " ++ show ty1 ++ "\n ty2 = " ++ show ty2 withoutSig (ForallT tvs cxt ty) = ForallT tvs cxt (withoutSig ty) withoutSig (AppT ty1 ty2) = AppT (withoutSig ty1) (withoutSig ty2) withoutSig (SigT ty ki) = withoutSig ty withoutSig ty = ty -- test #2: type quotations and reified types should agree wrt -- promoted tuples. ty1 <- [t| D '(True, False) |] ty2 <- [t| D (False, True) |] ClassI _ insts <- reify ''D let [ty1', ty2'] = map (withoutSig . getType) insts when (ty1 /= ty1') $ failMsg "C" ty1 ty1' when (ty2 /= ty2') $ failMsg "D" ty2 ty2' return [] }}} According to @RyanlGlScott in https://phabricator.haskell.org/D2188#79228 the code `D (True, False)` in regular Haskell code would be rejected as a Kind error, whereas when its in Oxford brackets like `[t| D (True, False) |]`, it manages to sneak through the type checker. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12853 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12853: Unpromoted tuples in TH in correctly accepted by tthe type checker -------------------------------------+------------------------------------- Reporter: erikd | Owner: Type: bug | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler (Type | Version: 8.1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Other | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Description changed by erikd: @@ -14,1 +14,0 @@ - class C (a :: Bool) @@ -16,4 +15,0 @@ - class E (a :: [Bool]) - - instance C True - instance C 'False @@ -23,3 +18,0 @@ - - instance E '[True, False] - instance E '[False, True] New description: This issue was discovered when writing tests for #11629. Test case: {{{#!hs {-# LANGUAGE DataKinds #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE FlexibleInstances #-} module T11629 where import Control.Monad import Language.Haskell.TH class D (a :: (Bool, Bool)) instance D '(True, False) instance D '(False, True) do let getType (InstanceD _ _ ty _) = ty getType _ = error "getType: only defined for InstanceD" failMsg a ty1 ty2 = fail $ "example " ++ a ++ ": ty1 /= ty2, where\n ty1 = " ++ show ty1 ++ "\n ty2 = " ++ show ty2 withoutSig (ForallT tvs cxt ty) = ForallT tvs cxt (withoutSig ty) withoutSig (AppT ty1 ty2) = AppT (withoutSig ty1) (withoutSig ty2) withoutSig (SigT ty ki) = withoutSig ty withoutSig ty = ty -- test #2: type quotations and reified types should agree wrt -- promoted tuples. ty1 <- [t| D '(True, False) |] ty2 <- [t| D (False, True) |] ClassI _ insts <- reify ''D let [ty1', ty2'] = map (withoutSig . getType) insts when (ty1 /= ty1') $ failMsg "C" ty1 ty1' when (ty2 /= ty2') $ failMsg "D" ty2 ty2' return [] }}} According to @RyanlGlScott in https://phabricator.haskell.org/D2188#79228 the code `D (True, False)` in regular Haskell code would be rejected as a Kind error, whereas when its in Oxford brackets like `[t| D (True, False) |]`, it manages to sneak through the type checker. -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12853#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12853: Unpromoted tuples in TH in correctly accepted by the type checker -------------------------------------+------------------------------------- Reporter: erikd | Owner: Type: bug | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler (Type | Version: 8.1 checker) | Keywords: Resolution: | TemplateHaskell Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Other | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * keywords: => TemplateHaskell * cc: RyanGlScott, goldfire (added) Comment: I think there are two unrelated issues at play here. One is the issue that there's an inconsistency between tuples and other type constructors w.r.t. automatic promotion. Namely, most types get automatically promoted to a kind in certain contexts, whereas tuples do not. This is why `ty2`'s TH AST doesn't match that of `ty2'`. The other issue is that this program even typechecks at all. In light of the fact that tuples don't automatically get promoted to kinds, something like `[t| D (Bool, Bool) |]` feels bogus. But you can make it even more bogus if you wanted to: {{{#!hs ty2 <- [t| D (Char, Maybe) |] }}} For better or worse, TH doesn't appear to kind-check its quoted types until they're spliced. Is this desirable? On hand, this allows you to pass around values in `Q` computations that don't necessarily type-check, which can be convenient. On the other hand, not sanity checking TH quotations leads to bizarre results like in the program above. I'm a bit reticent to say we should change the behavior with regards to the second issue, since I feel like it could be a very disruptive breaking change. I've cc'd goldfire to get his opinion on the matter. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12853#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12853: Unpromoted tuples in TH in correctly accepted by the type checker -------------------------------------+------------------------------------- Reporter: erikd | Owner: Type: bug | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler (Type | Version: 8.1 checker) | Keywords: Resolution: | TemplateHaskell Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Other | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by rwbarton):
For better or worse, TH doesn't appear to kind-check its quoted types until they're spliced.
It's consistent with TH not type checking quoted expressions. And in general the quotation could contain a splice, in which it can't be checked. So, there seems to be no issue here, actually? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12853#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12853: Unpromoted tuples in TH in correctly accepted by the type checker -------------------------------------+------------------------------------- Reporter: erikd | Owner: Type: bug | Status: closed Priority: normal | Milestone: 8.2.1 Component: Compiler (Type | Version: 8.1 checker) | Keywords: Resolution: invalid | TemplateHaskell Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Other | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => closed * resolution: => invalid Comment: Replying to [comment:3 rwbarton]:
It's consistent with TH not type checking quoted expressions. And in general the quotation could contain a splice, in which it can't be checked.
So, there seems to be no issue here, actually?
Upon further thought, I think you're right. I'll close this as invalid, then. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12853#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC