Conor McBride wrote:
Just imagine
data Eq a b where Refl :: Eq a a
coerce :: Eq a b -> a -> b Robert Dockins wrote:
coerce ~Refl x = x
coerce undefined True :: String
Bang you're dead. Or rather... Twiddle you're dead.
Mom, he's scaring me! ;) Who says this function may not be strict in the first argument despite the irrefutable pattern? Also, for the sarcastically inclined, death is semantically equivalent to _|_. As is (fix id :: a -> b), too. Alas, one can say dontcoerce :: Eq a (Maybe b) -> a -> Maybe b dontcoerce ~Refl x = Just x and dontcoerce' _|_ ==> (\x -> Just (x :: b(~Refl))) ==> \(x::_|_) -> Just (x :: _|_) ==> \_ -> Just _|_ The type of x on the right-hand side inherently depends on ~Refl and should be _|_ if ~Refl is. Type refinement makes the types depend on values, after all. For our optimization problem, it's only a matter of constructors on the right hand side. They should pop out before do not look on any arguments, so it's safe to cry "so you just know, i'm a Just". Maybe one can remedy things by introducing a _|_ on type-level with the only inhabitant _|_ :: _|_. That would treat objections Ross Paterson referenced:
See the second restriction. Irrefutable patterns aren't mentioned there, but they're the general case. See also
http://www.haskell.org/pipermail/haskell-cafe/2006-May/015609.html http://www.haskell.org/pipermail/glasgow-haskell-users/2006-May/010278.html
Admittedly, it's a thin ice to trample on, but otherwise, for this special splitSeq-problem, one runs into the "more haste less speed" dilemma (i mean Wadler's paper ). Bertram's lazy algorithm actually is an online-algorithm and it should remain one when making it type safe. Regards, apfelmus