Edward Kmett suggests the use of @ instead of ! Edward Kmett wrote: This is just a form of refinement type. Googling the term should turn up a couple dozen papers on the topic. You can emulate them (and more) with phantom types in the existing type system, though admittedly the encoding is occasionally uncomfortable. As a result there hasn't been much interest in them from on high. And a minor technical issue with the use of ! there is that it would be awkward from a grammar perspective because it would require that ! bind more tightly than juxtaposition, but only when parsing a type. Another syntactic operator like @ that already binds very tightly might be more appropriate. -Edward Kmett New proposal draft: Proposal: Type supplement for constructor specific uses of sum types Purpose: Avoid error clauses (runtime errors), exception control or Maybe types in partially defined (constructor specific) functions on sum types. As an example, with data List a = Nil | Cons a (List a) * Actual system, with runtime errors (as in GHC Data.List head) or exception throwing or optional Maybe results. hd :: List a -> a hd (Cons x _) -> x hd Nil -> error "error: hd: empty list" -- error or exception throwing * Proposed system extending types with a suffix @ Constructor or @ {Constructor1, Constructor2, ..} hd :: List @ Cons a -> a hd (Cons x _) = x The caller must do pattern matching before applying the constructor-specific function. In ''var @ (Constructor {})'' the compiler should set a type supplement property for ''var'' to the specified pattern constructor and check the supplement when used in a constructor specific parameter position. using it: accumHead :: (a->b) -> a -> List a -> b accumHead f accum list = case list of li @ Cons {} -> f accum $ hd li -- typeSupplementOf li == 'Cons' -- should pass typechecker at ''hd'' for List!Cons li @ Nil -> f accum $ hd li -- compiler error !! -- typeSupplementOf li == 'Nil' ; no match _ -> f accum $ hd list -- compiler error !! -- typeSupplementOf list == Nothing ; no match _ -> accum -- default closing pattern matching exhaustivity. (from Jason Dagit contribution) For more than one constructor say data List2 a = Nil | Cons a (List2 a) | Cons2 a a (List2 a) hd :: List2 @ {Cons, Cons2} a -> a