Changes between Initial Version and Version 6 of Ticket #8422


Ignore:
Timestamp:
Jan 23, 2016 12:28:55 PM (4 years ago)
Author:
thomie
Comment:

Legend:

Unmodified
Added
Removed
Modified
  • Ticket #8422

    • Property Priority changed from highest to normal
    • Property Cc diatchki added
    • Property Keywords TypeLits added
    • Property Milestone changed from 7.8.1 to 8.0.1
  • Ticket #8422 – Description

    initial v6  
    11I 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!)
    22
     3{{{#!hs
     4{-# LANGUAGE DataKinds #-}
     5{-# LANGUAGE GADTs #-}
     6{-# LANGUAGE KindSignatures #-}
     7{-# LANGUAGE TypeOperators #-}
     8module Fancy where
     9
     10import GHC.TypeLits
     11
     12infixr 3 :*
     13 
     14data Shape (rank :: Nat) where
     15    Nil  :: Shape 0
     16    (:*) :: {-# UNPACK #-} !(Int :: *) -> !(Shape r) -> Shape (1 + r)
     17
     18reverseShape :: Shape r -> Shape r
     19reverseShape Nil = Nil
     20reverseShape shs = go shs Nil
     21    where
     22        go :: Shape a -> Shape b -> Shape (a+b)
     23        go Nil res = res
     24        go (ix :* more ) res = go more (ix :* res)
     25}}}