Opened 4 years ago
Last modified 2 years ago
#8422 new bug
type nats solver is too weak!
Reported by: | carter | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | |
Component: | Compiler (Type checker) | Version: | 7.7 |
Keywords: | TypeLits | Cc: | diatchki |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | GHC rejects valid program | Test Case: | |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Rev(s): | ||
Wiki Page: |
Description (last modified by )
I just built ghc HEAD today, and the type nat solver can't handle the attached program, which *should* be simple to check! (and while I could use unsafeCoerce to "prove" it correct, that defeats the purpose of having the type nat solver!)
{-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE TypeOperators #-} module Fancy where import GHC.TypeLits infixr 3 :* data Shape (rank :: Nat) where Nil :: Shape 0 (:*) :: {-# UNPACK #-} !(Int :: *) -> !(Shape r) -> Shape (1 + r) reverseShape :: Shape r -> Shape r reverseShape Nil = Nil reverseShape shs = go shs Nil where go :: Shape a -> Shape b -> Shape (a+b) go Nil res = res go (ix :* more ) res = go more (ix :* res)
Attachments (1)
Change History (8)
Changed 4 years ago by
comment:1 Changed 4 years ago by
the error in question is
Fancy.hs:58:35: Could not deduce ((r2 + (1 + b)) ~ (a + b)) from the context (r ~ (1 + r1)) bound by a pattern with constructor :* :: forall (r :: Nat). Int -> Shape r -> Shape (1 + r), in an equation for ‛reverseShape’ at Fancy.hs:54:19-30 or from (a ~ (1 + r2)) bound by a pattern with constructor :* :: forall (r :: Nat). Int -> Shape r -> Shape (1 + r), in an equation for ‛go’ at Fancy.hs:58:13-22 NB: ‛+’ is a type function, and may not be injective Expected type: Shape (a + b) Actual type: Shape (r2 + (1 + b)) Relevant bindings include res :: Shape b (bound at Fancy.hs:58:27) more :: Shape r2 (bound at Fancy.hs:58:19) go :: Shape a -> Shape b -> Shape (a + b) (bound at Fancy.hs:57:9) In the expression: go more (ix :* res) In an equation for ‛go’: go (ix :* more) res = go more (ix :* res)
in one case , the solver should be able to deduce that 0+b = b ===> b = r and in the other case that a = a_1+1 then (a+b =r ) implies a_1 + b +1=r
or something like that
comment:2 Changed 4 years ago by
i tried getting solver example in the status report to work, and it doesn't :(
comment:3 Changed 4 years ago by
Cc: | diatchki added |
---|---|
Milestone: | 7.8.1 → 7.10.1 |
Priority: | highest → normal |
This shouldn't be highest priority.
The example is the status report isn't literal. The solver works as expected if you give it terms to think about, but perhaps it should be reworded. If you have a problem with something this simple, we need an example.
But the core problem with your example is that the solver doesn't recognize that +
is associative, as Richard pointed out in #8423 (but you can get around this with a manual proof term defined inductively. at least.) For example, I believe plus_succ
here should typecheck without issue.
In any case, this probably won't be solved in the 7.8 timeframe, but I've added Iavor to the ticket in case he wants to correct me or clarify something.
{-# LANGUAGE DataKinds, TypeOperators #-} module Main where import GHC.TypeLits import Data.Proxy import Data.Type.Equality witness1 :: Proxy x -> Proxy (x+2) witness1 _ = Proxy -- This typechecks ex1 :: Proxy 5 ex1 = witness1 (Proxy :: Proxy 3) -- This does not --ex2 :: Proxy 5 --ex2 = witness1 (Proxy :: Proxy 4) -------------------------------------------------------------------------------- -- Proof of zero identity plus_id :: Proxy n -> (n+0 :~: n) plus_id _ = Refl -- Proof of associativity -- -- This doesn't typecheck --plus_succ :: Proxy n1 -> Proxy n2 -> (n1+(n2+1) :~: (n1+n2)+1) --plus_succ _ _ = Refl
comment:4 Changed 3 years ago by
Milestone: | 7.10.1 → 7.12.1 |
---|
Moving to 7.12.1 milestone; if you feel this is an error and should be addressed sooner, please move it back to the 7.10.1 milestone.
comment:6 Changed 2 years ago by
Description: | modified (diff) |
---|---|
Keywords: | TypeLits added |
comment:7 Changed 2 years ago by
Milestone: | 8.0.1 |
---|
fancy type nat fun