dima-starosud

defmodule Impl do
  defstruct value: 100

  def runImpl(%Impl{value: value}, x, y) do
    value + x + y
  end
end

defprotocol Runnable do
  def run(r, x, y)

dima-starosud

{-# LANGUAGE TypeFamilies, GADTs #-}

data OfInt (f :: * -> *) where
    OfInt :: f Int -> OfInt f

type family F a where
    F a = Maybe a

runF :: F Int -> OfInt F
runF = OfInt {- Error on this line:

dima-starosud

open import Function
open import Relation.Binary.PropositionalEquality
open import Data.Product
open import Data.String
open import Data.Bool
open import Data.Unit

record Level : Set where
  constructor level
  field

dima-starosud

open import Function
open import Relation.Binary.PropositionalEquality
open import Data.Product
open import Data.String
open import Data.Bool
open import Data.Unit

record Level : Set where
  constructor level

dima-starosud

{-# LANGUAGE DataKinds
           , KindSignatures
           , TypeFamilies
           , GADTs
           , TypeOperators
           , ScopedTypeVariables
           , MultiParamTypeClasses
           , FlexibleInstances
           , StandaloneDeriving
           , RankNTypes