[GHC] #14203: GHC-inferred type signature doesn't actually typecheck
#14203: GHC-inferred type signature doesn't actually typecheck -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 (Type checker) | Keywords: TypeInType, | Operating System: Unknown/Multiple TypeFamilies | Architecture: | Type of failure: GHC rejects Unknown/Multiple | valid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- This code typechecks: {{{#!hs {-# LANGUAGE GADTs #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} module Bug where import Data.Kind data TyFun :: * -> * -> * type a ~> b = TyFun a b -> * infixr 0 ~> type family Apply (f :: k1 ~> k2) (x :: k1) :: k2 data family Sing :: k -> * data Sigma (a :: *) :: (a ~> *) -> * where MkSigma :: forall (a :: *) (p :: a ~> *) (x :: a). Sing x -> Apply p x -> Sigma a p data instance Sing (z :: Sigma a p) where SMkSigma :: Sing sx -> Sing px -> Sing (MkSigma sx px) }}} I was curious to know what the full type signature of `SMkSigma` was, so I asked GHCi what the inferred type is: {{{ λ> :i SMkSigma data instance Sing z where SMkSigma :: forall a (p :: a ~> *) (x :: a) (sx :: Sing x) (px :: Apply p x). (Sing sx) -> (Sing px) -> Sing ('MkSigma sx px) }}} I attempted to incorporate this newfound knowledge into the program: {{{#!hs {-# LANGUAGE GADTs #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} module Bug where import Data.Kind data TyFun :: * -> * -> * type a ~> b = TyFun a b -> * infixr 0 ~> type family Apply (f :: k1 ~> k2) (x :: k1) :: k2 data family Sing :: k -> * data Sigma (a :: *) :: (a ~> *) -> * where MkSigma :: forall (a :: *) (p :: a ~> *) (x :: a). Sing x -> Apply p x -> Sigma a p data instance Sing (z :: Sigma a p) where SMkSigma :: forall a (p :: a ~> *) (x :: a) (sx :: Sing x) (px :: Apply p x). Sing sx -> Sing px -> Sing (MkSigma sx px) }}} But to my surprise, adding this inferred type signature causes the program to no longer typecheck! {{{ GHCi, version 8.3.20170907: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Bug ( Bug.hs, interpreted ) Bug.hs:23:31: error: • Expected kind ‘Apply p0 x’, but ‘px’ has kind ‘Apply p1 x’ • In the first argument of ‘Sing’, namely ‘px’ In the type ‘Sing px’ In the definition of data constructor ‘SMkSigma’ | 23 | Sing sx -> Sing px -> Sing (MkSigma sx px) | ^^ }}} I'm showing the output of GHC HEAD here, but this bug can be reproduced all the way back to GHC 8.0.1. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14203 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14203: GHC-inferred type signature doesn't actually typecheck -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Keywords: TypeInType, Resolution: | TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Here's a slightly simpler example that doesn't use `singletons`. This compiles: {{{#!hs {-# LANGUAGE GADTs #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} module Bug where import Data.Kind data TyFun :: * -> * -> * type a ~> b = TyFun a b -> * infixr 0 ~> type family Apply (f :: k1 ~> k2) (x :: k1) :: k2 data Foo (z :: Apply (p :: a ~> *) (x :: a)) data Bar where MkBar :: Foo z -> Bar }}} And if you ask GHCi for the type of `MkBar`, you get: {{{ λ> :type +v MkBar MkBar :: forall a (p :: TyFun a * -> *) (x :: a) (z :: Apply p x). Foo z -> Bar }}} But if you try using that: {{{#!hs {-# LANGUAGE GADTs #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} module Bug where import Data.Kind data TyFun :: * -> * -> * type a ~> b = TyFun a b -> * infixr 0 ~> type family Apply (f :: k1 ~> k2) (x :: k1) :: k2 data Foo (z :: Apply (p :: a ~> *) (x :: a)) data Bar where MkBar :: forall a (p :: TyFun a * -> *) (x :: a) (z :: Apply p x). Foo z -> Bar }}} It fails: {{{ GHCi, version 8.3.20170907: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Bug ( Bug.hs, interpreted ) Bug.hs:19:16: error: • Expected kind ‘Apply p0 x0’, but ‘z’ has kind ‘Apply p x’ • In the first argument of ‘Foo’, namely ‘z’ In the type ‘Foo z’ In the definition of data constructor ‘MkBar’ | 19 | Foo z -> Bar | ^ }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14203#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14203: GHC-inferred type signature doesn't actually typecheck -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Keywords: TypeInType, Resolution: | TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): The original programs should be rejected, I think. Looking at your simpler example, the declaration for `Foo` should be rejected as ambiguous. There's no way to tell from `z` what `a`, `x`, or `p` should be. When I continue my bug sweep, I'll take a look at this. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14203#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14203: GHC-inferred type signature doesn't actually typecheck -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Keywords: TypeInType, Resolution: | TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): I can accept that the second program (with `MkBar`) would be ambiguous, but I don't understand what is wrong with the original program (with `SMkSigma`), especially the form when an explicit `forall`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14203#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14203: GHC-inferred type signature doesn't actually typecheck -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Keywords: TypeInType, Resolution: | TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): The type of `SMkSigma` is also ambiguous. There's no way to infer `p` from the visible arguments. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14203#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14203: GHC-inferred type signature doesn't actually typecheck -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Keywords: TypeInType, Resolution: | TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Huh, that's interesting... how do you resolve such an ambiguity, then? Normally, my approach is to add proxies until the ambiguity is resolved, such as what I tried below: {{{#!hs {-# LANGUAGE GADTs #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} module Bug where import Data.Kind import Data.Proxy data TyFun :: * -> * -> * type a ~> b = TyFun a b -> * infixr 0 ~> type family Apply (f :: k1 ~> k2) (x :: k1) :: k2 data family Sing :: k -> * data Sigma (a :: *) :: (a ~> *) -> * where MkSigma :: forall (a :: *) (p :: a ~> *) (x :: a). Sing x -> Apply p x -> Sigma a p data instance Sing (z :: Sigma a p) where SMkSigma :: forall a (p :: a ~> *) (x :: a) (sx :: Sing x) (px :: Apply p x). Proxy a -> Proxy p -> Proxy x -> Sing sx -> Sing px -> Sing (MkSigma sx px) }}} But that still results in the same error. Adding `AllowAmbiguousTypes` doesn't help either. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14203#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14203: GHC-inferred type signature doesn't actually typecheck -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Keywords: TypeInType, Resolution: | TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Actually, it's not just limited to datatypes: the same effect can be observed in this program: {{{#!hs {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} module Bug where type family F a data Foo (z :: F a) bar :: forall a (z :: F a). Foo z -> Int bar _ = 42 }}} {{{ $ /opt/ghc/8.2.1/bin/ghci Bug.hs GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/ryanglscott/.ghci [1 of 1] Compiling Bug ( Bug.hs, interpreted ) Bug.hs:10:33: error: • Expected kind ‘F a0’, but ‘z’ has kind ‘F a’ • In the first argument of ‘Foo’, namely ‘z’ In the type signature: bar :: forall a (z :: F a). Foo z -> Int | 10 | bar :: forall a (z :: F a). Foo z -> Int | ^ }}} Here, I would expect `AllowAmbiguousTypes` to squash the error message about the ambiguous variable `a0` in `F a0`, but that doesn't happen. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14203#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14203: GHC-inferred type signature doesn't actually typecheck -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Keywords: TypeInType, Resolution: | TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): In comment:6 we have {{{ Foo :: forall a. F a -> * }}} That's an ambiguous kind! Just like for a function {{{ foo :: forall k. F k -> Int }}} is ambiguous. So all uses of `Foo` will give rise to ambiguity. But alas we do not check for ambiguous kinds. Instead we see a "call" of `Foo` in the type signature {{{ bar :: forall a (z :: F a). Foo z -> Int }}} At the use of `Foo` we intantiate `k` to `kappa` and check that `F kappa` is equal o the kind of `z` namely `F a`. So for the type to be well- kinded we need `F kappa ~ F a`. But we have no way to prove that (unless `F` is injective). And that's the error. TL;DR: it's `Foo` that should be rejected as having an ambiguous kind. (I have not studied the oroginal Description; just assuming that comment:6 embodies the essence.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14203#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14203: GHC-inferred type signature doesn't actually typecheck -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Keywords: TypeInType, Resolution: | TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): I'm well aware of the fact that this is an ambiguous definition. But the point that I'm making (that no one has addressed yet) is that `AllowAmbiguousTypes` should allow GHC to accept such a definition! Replying to [comment:7 simonpj]:
But alas we do not check for ambiguous kinds.
If we don't do this currently, then we should! There are many programs that I can't write because of this restriction. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14203#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14203: GHC-inferred type signature doesn't actually typecheck -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Keywords: TypeInType, Resolution: | TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj):
But the point that I'm making (that no one has addressed yet) is that AllowAmbiguousTypes should allow GHC to accept such a definition!
If we don't do this currently, then we should! There are many programs
I don't agree. It's the definition of `Foo` that has an ambiguous kind. ThE type signature for `bar` is entirely innocent. To see this more clearly try {{{ bar :: forall a (z :: F a). Foo z -> Proxy z -> Int }}} Nothing ambiguous about that. But simply kind-checking the type signature fails because `Foo`'s kind is ambiguous. that I can't write because of this restriction. ] What is "this"? Rejecting the definition of `Foo` (which would be the effect of checking `Foo`'s kind for ambiguity) would not typecheck more programs! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14203#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14203: GHC-inferred type signature doesn't actually typecheck -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Keywords: TypeInType, Resolution: | TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Replying to [comment:9 simonpj]:
I don't agree. It's the definition of `Foo` that has an ambiguous kind.
What is "this"? Rejecting the definition of `Foo` (which would be the effect of checking `Foo`'s kind for ambiguity) would not typecheck more
OK, sure. The point is—there's //some// definition in this program with an ambiguous kind, and `AllowAmbiguousTypes` is not convincing GHC to accept it. If the burden of ambiguity proof needs to be shifted to `Foo` instead, that's fine. programs! The point is that I //want// GHC to accept `Foo` (and `bar`). The mechanism by which I normally do so (`AllowAmbiguousTypes`) is failing me here. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14203#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14203: GHC-inferred type signature doesn't actually typecheck -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Keywords: TypeInType, Resolution: | TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): I don't see how you want GHC to accept `bar`. Let's take this slowly. ``` type family F a ``` So far, so good. ``` data Foo (z :: F a) ``` As Simon points out, `Foo` has an ambiguous kind `forall (a :: Type). F a -> Type`. There's no way to infer the choice of `a` from a usage of `Foo`. GHC does not check for ambiguous kinds (it should, I agree), so this definition is accepted with or without `AllowAmbiguousTypes`. Regardless, you've specified `AllowAmbiguousTypes`, so accepting this conforms to your stated desires. ``` bar :: forall a (z :: F a). Foo z -> Int ``` Now we're in deep trouble. This type mentions `Foo z`. Accordingly, GHC must infer the invisible kind parameter to `Foo`. (You might say "Well, obviously it should be `a`!", but that would be assuming `F` is injective.) So GHC rejects this type signature, as it doesn't know what the invisible kind parameter to `Foo` should be. Note that this is ''not'' the normal ambiguity check that `AllowAmbiguousTypes` disables. This type has an ambiguous type variable; the type itself is not ambiguous. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14203#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14203: GHC-inferred type signature doesn't actually typecheck -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Keywords: TypeInType, Resolution: | TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): OK. So what you're saying is that: {{{#!hs bar :: forall a (z :: F a). Foo z -> Int }}} Should be rejected as an ambiguous //occurrence// site (which `AllowAmbiguousTypes` does not permit) rather than an ambiguous //definition// site (which `AllowAmbiguousType` //does// permit)? I could buy that, although I'm a bit miffed that there doesn't appear to be a satisfying way to resolve the ambiguity. In an ideal world, you could say: {{{#!hs bar :: forall (a :: k) (z :: F @k a). Foo z -> Int }}} But there's no visible kind application. In a fit of rage, I even tried giving kind signatures to //everything//: {{{#!hs {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} module Bug where type family F (a :: k) data Foo (z :: F (a :: k)) bar :: forall (a :: k) (z :: F (a :: k)). Foo (z :: F (a :: k)) -> Int bar _ = 42 }}} But that still produces the same error. So how am I supposed to proceed from here? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14203#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14203: GHC-inferred type signature doesn't actually typecheck -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Keywords: TypeInType, Resolution: | TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): You're not. Don't write a type with an ambiguous kind. :) Alternatively, and even better, implement visible kind application. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14203#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14203: GHC-inferred type signature doesn't actually typecheck -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Keywords: TypeInType, Resolution: | TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): OK, I found out how to do this. The trick is to make the kind of `a` in `F` visible: {{{#!hs {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} module Bug where type family F a data Foo a (z :: F a) bar :: forall a (z :: F a). Foo a z -> Int bar _ = 42 }}} A similar trick works for the program in comment:1: {{{#!hs {-# LANGUAGE GADTs #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} module Bug where import Data.Kind data TyFun :: * -> * -> * type a ~> b = TyFun a b -> * infixr 0 ~> type family Apply (f :: k1 ~> k2) (x :: k1) :: k2 data Foo p x (z :: Apply (p :: a ~> *) (x :: a)) data Bar where MkBar :: forall a (p :: TyFun a * -> *) (x :: a) (z :: Apply p x). Foo p x z -> Bar }}} Alas, this trick doesn't scale very well to the original program, since you'd need to give `p` as a visible argument to `Sing px` somehow. (It's not clear to me if even visible kind application would fix this problem.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14203#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14203: GHC-inferred type signature doesn't actually typecheck -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Keywords: TypeInType, Resolution: | TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj):
Should be rejected as an ambiguous occurrence site (which AllowAmbiguousTypes does not permit) rather than an ambiguous definition site (which AllowAmbiguousType does permit)?
Yes. Precisely like this case: {{{ {-# LANGUAGE AllowAmbiguousTypes #-} f :: F a -> Int -- Ambiguous, but allowed because of the pragma f = e boogle :: F b -> Int boogle v = f v }}} GHC instantiates `F` at `alpha` and then complains it can't equate `F b ~ F alpha`. Visible type application is the solution. The only thing happening in this ticket is that this very same pattern is manifesting at the type level instead of the term level. Nothing more! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14203#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14203: GHC-inferred type signature doesn't actually typecheck -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Keywords: TypeInType, Resolution: | TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): OK. So after these musings about `AllowAmbiguousTypes`, kind ambiguities, and visible kind application, I've lost track if there's actually any concrete GHC bug that's manifesting in the original program. Can this be closed, or is there something left to be done? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14203#comment:16 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14203: GHC-inferred type signature doesn't actually typecheck -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Keywords: TypeInType, Resolution: | TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): I think that comment:6 is not a bug. I have not analysed the more complex examples. If they are the same, let's indeed close. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14203#comment:17 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14203: GHC-inferred type signature doesn't actually typecheck -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Keywords: TypeInType, Resolution: invalid | TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => closed * resolution: => invalid -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14203#comment:18 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14203: GHC-inferred type signature doesn't actually typecheck -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Keywords: TypeInType, Resolution: invalid | TypeFamilies Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): I've just created #14419 to request an ambiguity check on kinds, which may have helped Ryan not to get caught in this trap. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14203#comment:19 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC