Opened 4 years ago

Last modified 15 months 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 thomie)

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)

Fancy.hs (3.5 KB) - added by carter 4 years ago.
fancy type nat fun

Download all attachments as: .zip

Change History (8)

Changed 4 years ago by carter

Attachment: Fancy.hs added

fancy type nat fun

comment:1 Changed 4 years ago by carter

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 carter

i tried getting solver example in the status report to work, and it doesn't :(

http://ghc.haskell.org/trac/ghc/wiki/Status/Oct13

comment:3 Changed 4 years ago by thoughtpolice

Cc: diatchki added
Milestone: 7.8.17.10.1
Priority: highestnormal

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 2 years ago by thoughtpolice

Milestone: 7.10.17.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:5 Changed 20 months ago by thoughtpolice

Milestone: 7.12.18.0.1

Milestone renamed

comment:6 Changed 15 months ago by thomie

Description: modified (diff)
Keywords: TypeLits added

comment:7 Changed 15 months ago by thomie

Milestone: 8.0.1
Note: See TracTickets for help on using tickets.