I have a multi-parameter typeclass with a functional dependency: class Multi a b | a -> b I also have a simple, non-injective type synonym family: type family Fam a I want to write an inst...

Messing around with GHC's DataKinds, I tried implementing type-level binary nats. They're simple enough to implement, but if I want them to be useful in common cases, then GHC needs to believe that...

I have a typeclass A with a non injective associated type Context class A a where type Context a so many instances of A can have the same Context. Some instances of A are also instances of the cl...

Is there any way to write a type family that sometimes evaluates to a constrained type such as C a => T? This question arose when I was writing the following type family: type family Function (c...

Take this code snippet (I changed the type family to a closed one after the various comments and answers mentioned it): -- a closed type family for which I won't define any instances type family Em...

I am quite new to type level programming in haskell and I'm stuck with the following example. It is a fragment of a type level type checker for a small dsl. I want the Find type family to return a ...

This recursive definition of T fails to type-check. class C a where type T a :: Type newtype Compose (f :: Type -> Type) (g :: Type -> Type) (a :: Type) = Compose {getCompose :: f (g a)} i...

I understand how to define both homogeneous and heterogeneous streams in Haskell. -- Type-invariant streams. data InvStream a where (:::) :: a -> InvStream a -> InvStream a -- Heterogeneous...

While I was going through the haskell-excercises questions. I saw the following code which creates an aggregate Constraint by applying each type to a Constraint constructor. In GHC it seems deeply ...

Oftentimes, whenever working with monoidal operators in Haskell (or in any other languages for that matter), I find myself asking "Wouldn't it be convenient if the language itself had support ...

Why is GHC inferring unification from coercibility of associated data, and why is it contradicting its own checked type signature to do so? The problem {-# LANGUAGE ExplicitForAll #-} {-# LANGUAGE ...

Summary I have a typeclass for which I want to write some 'generic terms'. I have two questions: Using :t to ask GHCi for the type of a generic term works, but using that inferred type fails- why?...

For example, if I have these weird types: {-# LANGUAGE TypeFamilies #-} type family WeirdFamily a type instance WeirdFamily () = Int type instance WeirdFamily (a, b) = (a, WeirdFamily b) Can I dis...

In the following example: {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeFamilyDependencies #-} {-# LANGUAGE PolyKinds #-} newtype A a b = A (a, b) type family F (x :: k) = (r :: k) | r -> x typ...

I am trying to use this blogpost's approach to higher-kinded data without dangling Identity functors for the trival case together with quantified-constraint deriving: {-# LANGUAGE TypeFamilies #-}...

My issue I have the following type family that splits arguments off of a function: type family SeparateArgs ( a :: Type ) :: ( Type, [Type] ) where SeparateArgs (a -> b) = SndCons2 a (Se...

I have wrapped up whole data family in a single existential: data Type = Numeric | Boolean data family Operator (t :: Type) data instance Operator 'Numeric = Add | Sub data instance Operator 'Bo...

GHC.TypeNats exports type family of the following signature: type family (m :: Nat) + (n :: Nat) :: Nat How can I import it explicitly? import GHC.TypeNats((+)) does not work, because it says t...

Consider following definition of a HList: infixr 5 :> data HList (types :: [*]) where HNil :: HList '[] (:>) :: a -> HList l -> HList (a:l) And a type family Map to map over typele...

I have the following code: {-# LANGUAGE TypeFamilies #-} type family Times (a :: Nat) (b :: Nat) :: Nat where Times Z n = Z Times (S m) n = Plus n (Times m n) I know that type families allow ...

To motivate this question, let's first recall a bog-standard Hoare-Dijkstra-style indexed monad, and the example instance of an indexed writer monad. For an indexed monad, we just require type ali...

I've got a type family defined as follows: type family Vec a (n :: Nat) where Vec a Z = a Vec a (S n) = (a, Vec a n) I'd like to assert that the result of applying this type family always fulf...

I'm looking at the references at the backpack wiki trying to understand in which cases the use of backpack would be considered appropriate over other Haskell features like type-classes and type-fam...

I tried this: {-# LANGUAGE TypeFamilyDependencies #-} module Injective where type family F (a :: *) = (fa :: *) | fa -> a convert :: F a ~ F b => a -> b convert x = x GHC 8.6.4 gave m...

In the routing section, the article says: We can see that the RenderRoute class defines an associated data type providing the routes for our application. What does associated data type mean?...