[GHC] #13775: Type family expansion is too lazy, allows accepting of ill-typed terms
#13775: Type family expansion is too lazy, allows accepting of ill-typed terms -------------------------------------+------------------------------------- Reporter: fizruk | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.2 (Type checker) | Keywords: | Operating System: MacOS X Architecture: x86_64 | Type of failure: GHC accepts (amd64) | invalid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- I'm using GHC 8.0.2 and I've just witnessed a weird bug. To reproduce a bug I use this type family, using `TypeError` (this is a minimal type family I could get to keep bug reproducible): {{{ {-# LANGUAGE DataKinds #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} import GHC.TypeLits type family Head xs where Head '[] = TypeError (Text "empty list") Head (x ': xs) = x }}} Then I go to GHCi, load this code and observe this: {{{
show (Proxy @ (Head '[])) "Proxy" }}}
This looks like a bug to me! I expect `Head '[]` to produce a type error. And indeed it does, if I ask differently: {{{
Proxy @ (Head '[])
<interactive>:9:1: error: • empty list • When checking the inferred type it :: Proxy (TypeError ...) }}} So far it looks like `show` somehow "lazily" evaluates it's argument type and that's why it's possible to `show Proxy` even when `Proxy` is ill- typed. But if I expand `Head '[]` manually then it all works as expected again: {{{
show $ Proxy @ (TypeError (Text "error"))
<interactive>:13:8: error: • error • In the second argument of ‘($)’, namely ‘Proxy @(TypeError (Text "error"))’ In the expression: show $ Proxy @(TypeError (Text "error")) In an equation for ‘it’: it = show $ Proxy @(TypeError (Text "error")) }}} You can remove `TypeError` from the original type family: {{{ type family Head xs where Head (x ': xs) = x }}} And it gets even weirder: {{{
show (Proxy @ (Head '[])) "Proxy" Proxy @ (Head '[]) Proxy }}}
I did not test this with GHC 8.2. I think this behaviour is not critical for me, but accepting ill-typed terms looks like a bad sign, especially for type-level-heavy programs. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13775 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13775: Type family expansion is too lazy, allows accepting of ill-typed terms -------------------------------------+------------------------------------- Reporter: fizruk | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.2 checker) | Keywords: Resolution: | CustomTypeErrors Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * keywords: => CustomTypeErrors * os: MacOS X => Unknown/Multiple * architecture: x86_64 (amd64) => Unknown/Multiple Comment: Also reproducible in GHC 8.2 and HEAD. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13775#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13775: Type family expansion is too lazy, allows accepting of ill-typed terms -------------------------------------+------------------------------------- Reporter: fizruk | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.2 checker) | Keywords: Resolution: | CustomTypeErrors Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by fizruk): By the way, if you mistype `Proxy` as `Prox`, you can also get GHC panic: {{{
Prox @ (Head '[]) ghc: panic! (the 'impossible' happened) (GHC version 8.0.2 for x86_64-apple-darwin): initTc: unsolved constraints WC {wc_insol = [W] Prox_a1L4 :: t_a1L3[tau:1] (CHoleCan: Prox) [W] Prox_a1Ls :: t_a1Lr[tau:1] (CHoleCan: Prox)}
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug }}} But this panic seems to be because of `TypeApplications` and can be reproduced with just two lines in GHCi: {{{
:set -XTypeApplications X @ Int ghc: panic! (the 'impossible' happened) (GHC version 8.0.2 for x86_64-apple-darwin): initTc: unsolved constraints WC {wc_insol = [W] X_a13x :: t_a13w[tau:1] (CHoleCan: X) [W] X_a13V :: t_a13U[tau:1] (CHoleCan: X)}
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug }}} Should I file this one separately? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13775#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13775: Type family expansion is too lazy, allows accepting of ill-typed terms -------------------------------------+------------------------------------- Reporter: fizruk | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.2 checker) | Keywords: Resolution: | CustomTypeErrors Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): That one is actually a known bug (#13466) which has been fixed in GHC 8.2.1. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13775#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13775: Type family expansion is too lazy, allows accepting of ill-typed terms -------------------------------------+------------------------------------- Reporter: fizruk | Owner: diatchki Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.2 checker) | Keywords: Resolution: | CustomTypeErrors Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * owner: (none) => diatchki Comment: This is really a question for Iavor, who implemented user-specified type errors. The [http://downloads.haskell.org/~ghc/master/users- guide/glasgow_exts.html#custom-compile-time-errors user manual section on custom errors] does not explain the behaviour of the feature (except with a single example), and need some serious love. What is happening is this: * GHC only reports custom type errors if * We have an ''unsolved'' constraint involving `TypeError` * We have a declared or inferred type involving `TypeError` * We get a constraint `Show (Proxy (TypeError "..."))`. * But the instance for `Proxy` is {{{ instance Show (Proxy s) where ... }}} so the `TypeError...` is discarded. * All constraints are solved, so no error is reported. Iavor: you may want to consider being more aggressive? Or at least documenting the expected behaviour better. Thanks! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13775#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13775: Type family expansion is too lazy, allows accepting of ill-typed terms -------------------------------------+------------------------------------- Reporter: fizruk | Owner: diatchki Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.2 checker) | Keywords: Resolution: | CustomTypeErrors Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by diatchki): I think that this is more a question about how type functions work, rather than `TypeError` specifically. Currently, GHC does not evaluate type functions unless it needs to, so there is no error reported. Similarly, GHC does not report any errors for the following example, which has nothing to do with `TypeError`: {{{ type family F a test = show (Proxy @ (Proxy (F Int)) }}} This works just fine and prints `Proxy`, it does not report a missing instance for `F Int`. I don't really like this behavior of GHC, but that's an orthogonal issue. I am not sure how I could be more aggressive with `TypeError` without a bunch of special cases, and also, last time we discussed this people seemed to want the lazy behavior. I'll take on updating the manual to be more explicit about the behavior. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13775#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13775: Type family expansion is too lazy, allows accepting of ill-typed terms -------------------------------------+------------------------------------- Reporter: fizruk | Owner: diatchki Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.2 checker) | Keywords: Resolution: | CustomTypeErrors Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj):
I think that this is more a question about how type functions work, rather than TypeError specifically.
No, I don't think it is. GHC ''never'' reports an error simply becuase it tries to evaluate `TypeError ..`. Rather, that call is stuck. That in turn may mean that some constraint can't be solved. And then, when reporting unsolved constraints, GHC looks for any nested calls to `TypeError` and reports them rather than the constraint itself. You wrote this code! It's nothing to do with how much reduction takes place, IMHO. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13775#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13775: Type family expansion is too lazy, allows accepting of ill-typed terms -------------------------------------+------------------------------------- Reporter: fizruk | Owner: diatchki Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.2 checker) | Keywords: Resolution: | CustomTypeErrors Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by diatchki): I remember how the implementation works. My comment was about the fact that GHC is perfectly happy to treat "stuck" types as ordinary types without fully resolving them, which is why it can solve constraints such as `Show (Proxy (TypeError ...))`, or `Show (Proxy (F Int))`. A different design choice is to refuse to solve such constraints until GHC is sure that the type functions involved will produce a valid result, but that's not what we currently do. As a result, neither the `TypeError` nor the missing `F Int` instance are reported, and the `Show` constraint is happily solved, which is---perhaps---somewhat confusing. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13775#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13775: Type family expansion is too lazy, allows accepting of ill-typed terms -------------------------------------+------------------------------------- Reporter: fizruk | Owner: diatchki Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.2 checker) | Keywords: Resolution: | CustomTypeErrors Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Sorry -- I didn't mean to sound snarky!
A different design choice is to refuse to solve such constraints until GHC is sure that the type functions involved will produce a valid result
I think you are suggesting that * Don't do any work on a constraint that mentions `TypeError`. E.g. `C [TypeError ..]` would never be solved, regardless of the instances for `C`. That sounds attractive, but it's fragile. Suppose we had `[W] C [alpha]` where `alpha` is a unification variable. Can we use an instance declaration on that? Well, no; it might turn out that, after hundreds more simplification steps on other constraints mentioning `alpha`, that `alpha := TypeError...`. Or it might be `[W] C (F alpha)`, where eventually `alpha := Int`, and then we reduce `F Int` to `TypeError...`. So I don't see how to make this approach robustly implementable. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13775#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13775: Type family expansion is too lazy, allows accepting of ill-typed terms -------------------------------------+------------------------------------- Reporter: fizruk | Owner: diatchki Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.2 checker) | Keywords: Resolution: | CustomTypeErrors Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by tom-bop): Are we sure this has to do with `TypeError`s? I see the same problem without them: {{{#!haskell {-# LANGUAGE DataKinds #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} import GHC.TypeLits import Data.Proxy type family Head xs where -- As written, this compiles, and it also compiles if you uncomment either -- of these lines: -- Head '[] = 'True ~ 'False -- Head '[] = TypeError ('Text "empty list") Head (x ': xs) = x main = print $ show (Proxy::Proxy (Head '[])) }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13775#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13775: Type family expansion is too lazy, allows accepting of ill-typed terms -------------------------------------+------------------------------------- Reporter: fizruk | Owner: diatchki Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.2 checker) | Keywords: Resolution: | CustomTypeErrors Operating System: Unknown/Multiple | Architecture: Type of failure: GHC accepts | Unknown/Multiple invalid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Well we hvae {{{ instance Show (Proxy s) where ... }}} Notice that `s` is not used. So the instance will work just fine if `s` = `Head '[]`. I don't regard this as a bug (yet, anyway). It accepts more programs than at least some people expect; but well typed programs (ones that are accepted) don't go wrong at runtime, which is what we ask from our type system. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13775#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC